proposition: Lemma enfa_starI x (p : A1) : nfa_accept p x -> @enfa_accept enfa_star (Some p) x.
proof: Proof. elim: x p => /= [p H|a x IH p]. - apply: (@EnfaNone enfa_star _ None) => //. exact: EnfaFin. - case/exists_inP => q q1 /IH. exact: EnfaSome. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)