Context-free languages are recursively enumerable

A context-free language is presented by an unrestricted grammar (grammar T) carrying the extra grammar_context_free constraint, so dropping that constraint exhibits the very same grammar as a recursively-enumerable witness. The inclusion is therefore immediate.

theorem is_RE_of_is_CF {T : Type} {L : Language T} (h : is_CF L) : is_RE L

Every context-free language is recursively enumerable.

theorem CF_subclass_RE {T : Type} : CF ⊆ RE

Context-free languages form a subclass of the recursively enumerable languages.