proposition: Lemma bigOI (T : eqType) (xs :seq T) j (F : T -> pS) : j \in xs -> mprv (F j ---> \or_(i <- xs) F i).
proof: Proof. elim: xs => //= t xs IH. rewrite inE big_cons => /orP [/eqP -> |]. exact: axOIl. move => in_xs. rewrite -> IH => //. exact: axOIr. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions