proposition: Lemma bigABBA (T : eqType) (xs : seq T) (F : T -> kS) : mprv ((\and_(s <- xs) AX (F s)) ---> AX (\and_(s <- xs) F s)).
proof: Proof. elim: xs; first by drop; rewrite big_nil. move => t xs IH. rewrite !big_cons. by rewrite -> IH, axABBA. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions