proposition: Lemma re_to_nfa_correct (r : regexp char) : nfa_lang (re_to_nfa r) =i r.
proof: Proof. elim: r => [||a|s IHs |s IHs t IHt |s IHs t IHt] w //=. - by rewrite -dfa_to_nfa_correct inE /dfa_accept inE. - exact: nfa_eps_correct. - exact: nfa_char_correct. - rewrite nfa_star_correct. exact: star_eq. - by rewrite nfa_plus_correct /plus inE IHs IHt. - rewrite nfa_conc_correct. exact: conc_eq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)