Linear languages are recursively enumerable

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

theorem is_RE_of_is_Linear {T : Type} {L : Language T} (h : is_Linear L) : is_RE L

Every linear language is recursively enumerable.

theorem Linear_subclass_RE {T : Type} : Linear ⊆ RE

Linear languages form a subclass of the recursively enumerable languages.