proposition: Lemma sat_bigand (T:eqType) (s : seq T) F I : I |= \and_(i <- s) F i <-> forall x, x \in s -> I |= F x.
proof: Proof. elim: s => [|a s IH]; first by rewrite big_nil; split => // _; apply. rewrite big_cons sat_and IH. split => [[A B]x/predU1P[->//|]|A]. exact: B. split => [|x B]; apply: A; by rewrite ?mem_head // inE B orbT. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)