proposition: Lemma is_nfa_nfa e: is_nfa (nfa e).
proof: Proof. generalize (Thompson.is_enfa e). unfold nfa, is_nfa, is_enfa. cbn. intuition auto with mx_predicates. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation