proposition: Lemma nfa_plus_correct (N M : nfa) : nfa_lang (nfa_plus N M) =i plus (nfa_lang N) (nfa_lang M).
proof: Proof. move => w. apply/idP/idP. - case/exists_inP => [[s|s]]; rewrite !inE => A B; apply/orP;[left|right];apply/exists_inP; exists s => //. + elim: w s {A} B => /= [|a w IH] s; first by rewrite inE. case/exists_inP => [[|]// p A /IH B]. apply/exists_inP. by exists p. + elim: w s {A} B => /= [|a w IH] s; first by rewrite inE. case/exists_inP => [[|]// p A /IH B]. apply/exists_inP. by exists p. - rewrite !inE. case/orP => /exists_inP [s A B]; apply/exists_inP; [exists(inl s)|exists(inr s)]; rewrite ?inE //. + elim: w s {A} B => /= [|a w IH] s; first by rewrite inE. case/exists_inP => [p A /IH B]. apply/exists_inP. by exists (inl p). + elim: w s {A} B => /= [|a w IH] s; first by rewrite inE. case/exists_inP => [p A /IH B]. apply/exists_inP. by exists (inr p). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)