proposition: Lemma and_sub (T : eqType) (xs ys : seq T) (F : T -> pS) : {subset xs <= ys} -> mprv ((\and_(i <- ys) F i) ---> \and_(j <- xs) F j).
proof: Proof. move => H. apply: bigAI => s /H. exact: bigAE. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions