proposition: Lemma bigAI (T : eqType) s (r : seq T) F : (forall i, i \in r -> mprv (s ---> F i)) -> mprv (s ---> \and_(i <- r) F i).
proof: Proof. elim: r => [ _ |x r IH H]; first by rewrite big_nil; mp; [K|]. rewrite big_cons. apply: rAI; first by apply: H; rewrite mem_head. apply: IH => i Hi. apply: H. by rewrite inE Hi orbT. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions