proposition: Lemma enfa_star_langI x : x \in nfa_lang A1 -> @enfa_accept enfa_star None x.
proof: Proof. case/exists_inP => s s1 s2. apply: (@EnfaNone enfa_star _ (Some s)) => //. exact: enfa_starI. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)