proposition: Lemma enfa_concIl (p : A1) x1 x2 : nfa_accept p x1 -> x2 \in nfa_lang A2 -> @enfa_accept enfa_conc (inl p) (x1++x2).
proof: Proof. elim: x1 p => /= [p Hp /exists_inP [q q1 q2]|a x1 IH p /exists_inP [q q1 q2] H]. - apply: (@EnfaNone enfa_conc _ (inr q)). by rewrite /= Hp. exact: enfa_concIr. - apply: (@EnfaSome enfa_conc _ _ (inl q)). by rewrite /= q1. exact: IH. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)