proposition: Theorem lang_eval e: lang e ≡ elang e.
proof: Proof. unfold lang. intro w. revert e. induction w as [|a w IH]; intro e; simpl derivs. - apply epsilon_iff_lang_nil. - rewrite IH. apply eval_deriv. Qed.
imports: syntax kleene boolean lang lset sums normalisation