proposition: Lemma nfa_ofP x : reflect (enfa_lang x) (x \in nfa_lang nfa_of).
proof: Proof. apply: (iffP exists_inP) => [[p Hp1 Hp2]|[s Hs1 /enfaE [p Hp1 Hp2]]]. - case/bigcupP : Hp1 => s Hs H. exists s => //. by apply/enfaE; exists p. - exists p => //. by apply/bigcupP; exists s. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)