proposition: Lemma sig_big_dep_idem (I : finType) (J : I -> finType) (P : pred I) (Q : forall {i}, pred (J i)) (F : forall {i}, J i -> R) : \big[op/x]_(i | P i) \big[op/x]_(j : J i | Q j) F j = \big[op/x]_(p : {i : I & J i} | P (tag p) && Q (tagged p)) F (tagged p).
proof: Proof. pose s := [seq Tagged J j | i <- index_enum I, j <- index_enum (J i)]. rewrite [LHS]big_mkcond_idem big_mkcondl_idem. rewrite [RHS]big_mkcond_idem -[RHS](@perm_big _ s). rewrite big_allpairs_dep_idem/=; apply: eq_bigr => i _. by rewrite -big_mkcond_idem/=; case: P; rewrite // big1_idem. rewrite uniq_perm ?index_enum_uniq//. by rewrite allpairs_uniq_dep// => [|i|[i j] []]; rewrite ?index_enum_uniq. by move=> [i j]; rewrite ?mem_index_enum; apply/allpairsPdep; exists i, j. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)