proposition: Lemma enfa_concE (p : enfa_conc) x : enfa_accept p x -> match p with | inr p' => nfa_accept p' x | inl p' => exists x1 x2, [/\ x = x1 ++ x2, nfa_accept p' x1 & x2 \in nfa_lang A2] end.
proof: Proof. elim => {p x} [[?|?] /imsetP [q] // ? [->] //||]. - move => [p|p] a [q|q] x //. + move => pq _ [x1] [x2] [X1 X2 X3]. exists (a::x1); exists x2; subst; split => //. by apply/exists_inP; exists q. + move => pq _ Hq. by apply/exists_inP; exists q. - move => [p|p] [q|q] //= x /andP[Hp Hq] _ ?. exists [::]; exists x; split => //. by apply/exists_inP; exists q. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)