proposition: Lemma enfa_concIr (p : A2) x : nfa_accept p x -> @enfa_accept enfa_conc (inr p) x.
proof: Proof. elim: x p => [p Hp|a x IH p /= /exists_inP [q q1 q2]]. - constructor; solve [exact: imset_f|exact:mem_imset]. - apply: (@EnfaSome enfa_conc _ _ (inr q)) => //. exact: IH. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)