proposition: Lemma big_imfset2 key (A : finmempred I) (B : forall i, finmempred (J i)) (h : forall i : I, J i -> K) (F : K -> R) : {in [pred t : {i : I & J i} | A (tag t) & B _ (tagged t)] &, injective (fun t => h (tag t) (tagged t))} -> \big[op/idx]_(k <- imfset2 key h A B) F k = \big[op/idx]_(i <- enum_finmem A) \big[op/idx]_(j <- enum_finmem (B i)) F (h i j).
proof: Proof. move=> h_inj; rewrite eq_big_imfset2 //. rewrite -(map_allpairs (fun t => h (tag t) (tagged t)) (fun=> Tagged _)). by rewrite big_map big_allpairs_dep. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)