proposition: Lemma big_plus_seqP (T char : eqType) (r : seq T) w (F : T -> regexp char) : reflect (exists2 x, x \in r & w \in F x) (w \in \sigma_(i <- r) F i).
proof: Proof. elim: r w => [|r rs IHrs] w. rewrite big_nil; by constructor => [[x]]. rewrite big_cons; apply: (iffP plusP) => [[H|H]|[x]]. - exists r => //; by rewrite mem_head. - case/IHrs : H => x Hx ?. exists x => //. by rewrite in_cons Hx orbT. - rewrite in_cons; case/orP => [/eqP -> |]; auto => ? ?. right. apply/IHrs. by exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)