proposition: Lemma big_rec2 I r (P : pred I) F1 F2 (K_F : forall i y1 y2, P i -> K y1 y2 -> K (op1 (F1 i) y1) (op2 (F2 i) y2)) : K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i).
proof: Proof. by rewrite unlock; elim: r => //= i r; case: ifP => //; apply: K_F. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)