proposition: Lemma dfa_to_nfa_correct : dfa_lang A =i nfa_lang dfa_to_nfa.
proof: Proof. move => w. rewrite !inE /nfa_s /=. elim: w (dfa_s A) => [|b w IHw] x; rewrite accE /=. - apply/idP/existsP => [Fx|[y /andP [/set1P ->]]//]. exists x. by rewrite !inE eqxx. - rewrite IHw. apply/exists_inP/exists_inP. + case => y /set1P -> H. exists x; first exact: set11. apply/existsP. exists (dfa_trans x b). by rewrite H eqxx. + case => y /set1P -> {y} /existsP [z] /andP [] /eqP-> H. exists z; by rewrite ?set11. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)