proposition: Lemma nfa2_of_correct : (w \in dfa_lang A) = (w \in nfa2_lang nfa2_of_dfa).
proof: Proof. apply/idP/idP; rewrite -![_ \in _ A]topredE /=. - rewrite -{1}[w]drop0 /nfa2_lang -topredE /= inord1 => H. exact: nfa2_of_aux. - rewrite -{2}[w]drop0 -[0]/((@ord1 n).-1). case/exists_inP => p. exact: nfa2_of_aux2. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)