proposition: Lemma enfa_starP x : reflect (enfa_lang enfa_star x) (star (nfa_lang A1) x).
proof: Proof. apply: (iffP idP). - case/starP => vv H ->. elim: vv H => /= [_|v vv]. + exists None => //. exact: EnfaFin. + move => IH /andP[/andP [H1 H2] H3]. exists None => //. apply: enfa_star_cat (IH _) => //. exact: enfa_star_langI. - case => q. rewrite inE => /eqP-> {q}. exact: enfa_starE. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)