proposition: Theorem correct e: eval (enfa e) ≡ e.
proof: Proof. induction e; simpl enfa. apply eval_zer. apply eval_one. rewrite eval_pls. now apply cup_weq. rewrite eval_dot. now apply dot_weq. rewrite eval_str. now apply str_weq. apply eval_cst. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation