proposition: Lemma enfa_concP x : reflect (enfa_lang enfa_conc x) (conc (nfa_lang A1) (nfa_lang A2) x).
proof: Proof. apply: (iffP (@concP _ _ _ _)) => [[x1] [x2] [X1 [X2 X3]] |]. - case/exists_inP : X2 => s ? ?. exists (inl s); first solve [exact: imset_f|exact:mem_imset]. subst. exact: enfa_concIl. - move => [[s /imsetP [? ? [?]] /enfa_concE [x1] [x2] [? ? ?] |s]]; last by case/imsetP. exists x1; exists x2. repeat (split => //). apply/exists_inP. by exists s;subst. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)