proposition: Lemma sat_orI (T:eqType) (s : seq T) x F I : x \in s -> I |= F x -> I |= \or_(i <- s) F i.
proof: Proof. elim: s => // a s IH /predU1P [<-|/IH A]; rewrite big_cons sat_or; tauto. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)