proposition: Lemma nfa_eps_correct: nfa_lang (nfa_eps) =i pred1 [::].
proof: Proof. move => w. apply/exists_inP/idP. + move => [[]]. case: w => [|a w] //= _. by case/exists_inP. + move => /=. rewrite inE=>/eqP->. exists tt; by rewrite /= inE. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)