proposition: Theorem lang_lang' e: lang e ≡ lang' e.
proof: Proof. symmetry. intro w. revert e. induction w as [a|a i w IH]; simpl lang'; intro e. - apply epsilon_iff_lang_nil. - rewrite IH. apply deriv_traces. Qed.
imports: kat lsyntax positives sups glang comparisons boolean