proposition: Lemma bigOE (T : eqType) F (xs :seq T) (s : pS) : (forall j, j \in xs -> mprv (F j ---> s)) -> mprv ((\or_(i <- xs) F i) ---> s).
proof: Proof. elim: xs. move => _. rewrite big_nil. exact: axBE. move => t xs IH H. rewrite big_cons. rule axOE. exact: H (mem_head _ _). apply: IH => j in_xs. apply: H. by rewrite inE in_xs. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions