proposition: Lemma nfa_char_correct (a : char) : nfa_lang (nfa_char a) =1 pred1 [:: a].
proof: Proof. move => w /=. apply/exists_inP/eqP => [[p]|]. - rewrite inE => /eqP->. case: w => [|b [|c w]] /=; first by rewrite inE. + by case/exists_inP => [[/eqP->|//]]. + case/exists_inP => [[_|//]]. by case/exists_inP. - move->. exists false; first by rewrite inE. apply/exists_inP. exists true; by rewrite ?inE //=. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)