proposition: Lemma sat_orE (T:eqType) (s : seq T) F I : I |= \or_(i <- s) F i -> exists2 x, x \in s & I |= F x.
proof: Proof. elim: s => // [|a s IH]; first by rewrite big_nil. rewrite big_cons sat_or. case => [A|/IH [x A B]]; first by exists a => //; exact: mem_head. exists x => //. by rewrite inE A orbT. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)