proposition: Lemma nfa_to_dfa_correct : nfa_lang A =i dfa_lang nfa_to_dfa.
proof: Proof. move => w. rewrite !inE {2}/nfa_to_dfa /=. elim: w (nfa_s _) => [|a x IH] X; rewrite /= accE ?inE. - apply/existsP/set0Pn => [] [p] H; exists p; by rewrite inE in H *. - rewrite -IH /dfa_trans /=. apply/exists_inP/exists_inP. + case => p inX /exists_inP [q ? ?]. exists q => //. rewrite inE. apply/exists_inP. by exists p. + case => p. rewrite inE => /exists_inP [q] ? ? ?. exists q => //. apply/exists_inP. by exists p. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)