proposition: Lemma big_imfset key (h : I -> J) (A : finmempred _) (G : J -> R) : {in A &, injective h} -> \big[op/idx]_(j <- imfset key h A) G j = \big[op/idx]_(i <- enum_finmem A) G (h i).
proof: Proof. by move=> h_inj; rewrite eq_big_imfset// big_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)