proposition: Lemma nfa_inhabP N : reflect (exists w, w \in nfa_lang N) (nfa_inhab N).
proof: Proof. apply: (iffP (dfa_inhabP _)). - move => [x]. rewrite -nfa_to_dfa_correct. by exists x. - move => [x ?]. exists x. by rewrite -nfa_to_dfa_correct. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)