proposition: Lemma bigODr (T:eqType) (xs : seq T) (t : pS) (F : T -> pS) : mprv ((\or_(i <- xs) F i) :/\: t <--> (\or_(i <- xs) F i :/\: t)).
proof: Proof. rule axEI. - rule axAcase. apply: bigOE => j Hj. apply: rAIL. rewrite <- (bigOI _ Hj). exact: axI. - apply: bigOE => j Hj. rule axAcase. do 2 Intro. ApplyH axAI. Rev* 1. drop. exact: bigOI. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions