proposition: Lemma enum_imfset2 (T1 : choiceType) (T2 : T1 -> choiceType) (f : forall x, T2 x -> K) (p1 : finmempred T1) (p2 : forall x, finmempred (T2 x)) : {in [pred t | p1 (tag t) & p2 _ (tagged t)] &, injective (fun t : sigT T2 => f (tag t) (tagged t))} -> perm_eq (imfset2 key f p1 p2) [seq f x y | x <- enum_finmem p1, y <- enum_finmem (p2 x)].
proof: Proof. move=> f_inj; rewrite unlock. apply: uniq_perm => [||i]; rewrite ?seq_fset_uniq ?seq_fsetE //. rewrite allpairs_uniq_dep ?enum_finmem_uniq//. by move=> x; rewrite enum_finmem_uniq. move=> t0 t0' /allpairsPdep[t1 [t2]]; rewrite !enum_finmemE => -[tp1 tp2 ->/=]. move=> /allpairsPdep[t1' [t2']]; rewrite !enum_finmemE => -[t'p1 t'p2 ->/=]. by apply: (f_inj (Tagged _ _) (Tagged _ _)); rewrite ?inE/=; apply/andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)