proposition: Lemma big_pmorph I r (P : pred I) F : valid (\big[PCM.join/Unit]_(i <- r | P i) F i) -> f (\big[PCM.join/Unit]_(i <- r | P i) F i) = \big[op1/id1]_(i <- r | P i) f (F i).
proof: Proof. rewrite unlock; elim: r=>[|x r IH] //=; case: ifP=>// H V. by rewrite f_op // IH //; apply: validR V. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)