proposition: Lemma bigAE (T:eqType) (F : T -> pS) (xs : seq T) (s:T) : s \in xs -> mprv ((\and_(x <- xs) F x) ---> F s).
proof: Proof. elim: xs; first by rewrite in_nil. move => t xs IH. rewrite inE big_cons. case/orP; first by move/eqP->. move/IH => E. by rewrite <- E. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions