proposition: Lemma enfa_starE (o : enfa_star) x : enfa_accept o x -> if o is Some p then exists x1 x2, [/\ x = x1 ++ x2, nfa_accept p x1 & star (nfa_lang A1) x2] else star (nfa_lang A1) x.
proof: Proof. elim => {x o}. - move => [q|//]. by rewrite inE; move/eqP. - move => [p|] a [q|] x // H acc [x1] [x2] [H1 H2 H3]. exists (a::x1); exists x2. rewrite H1. split => //. by apply/exists_inP; exists q. - move => [p|] [q|] x //=. + move => *. by exists [::]; exists x. + move => H acc [x1] [x2] [H1 H2]. rewrite H1. apply: star_cat. by apply/exists_inP; exists q. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)