proposition: Lemma big_morph I r (P : pred I) F : f (\big[op2/id2]_(i <- r | P i) F i) = \big[op1/id1]_(i <- r | P i) f (F i).
proof: Proof. by rewrite unlock; elim: r => //= i r <-; rewrite -f_op -fun_if. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)