proposition: Lemma big_allpairs_dep I1 (I2 : I1 -> Type) J (h : forall i1, I2 i1 -> J) (r1 : seq I1) (r2 : forall i1, seq (I2 i1)) (F : J -> R) : \big[*%M/1]_(i <- [seq h i1 i2 | i1 <- r1, i2 <- r2 i1]) F i = \big[*%M/1]_(i1 <- r1) \big[*%M/1]_(i2 <- r2 i1) F (h i1 i2).
proof: Proof. elim: r1 => [|i1 r1 IHr1]; first by rewrite !big_nil. by rewrite big_cat IHr1 big_cons big_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)