proposition: Lemma is_enfa e: is_enfa (enfa e).
proof: Proof. Opaque Peano.plus. unfold is_enfa. induction e; cbn; intuition auto with mx_predicates. Transparent Peano.plus. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation