proposition: Lemma enfa_star_cat x1 x2 (p : enfa_star) : enfa_accept p x1 -> enfa_lang enfa_star x2 -> enfa_accept p (x1 ++ x2).
proof: Proof. elim => {p x1}. - move => p. rewrite inE => /eqP->. case => q. by rewrite inE => /eqP->. - move => p a q x /=. case: p => // p. case: q => // q pq ? IH H. exact: EnfaSome (IH H). - move => [p|] [q|] x //= p1 p2 IH H; exact: EnfaNone (IH H). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)