proposition: Lemma mem_imfset2 (T1 : choiceType) (T2 : T1 -> choiceType) (f : forall x, T2 x -> K) (g := fun t : {x : T1 & T2 x} => f (tag t) (tagged t)) (p1 : finmempred T1) (p2 : forall x, finmempred (T2 x)) (x : T1) (y : T2 x) : injective g -> f x y \in imfset2 key f p1 p2 = (in_mem x p1) && (in_mem y (p2 x)).
proof: Proof. move=> f_inj; rewrite unlock seq_fsetE. apply/allpairsPdep/idP => [[t1 [t2]]|]; last first. by move=> /andP[xp1 xp2]; exists x, y; rewrite ?enum_finmemE. rewrite !enum_finmemE => -[pt1 pt2]; elim/(TaggedP T2): _ / t2 => t in pt1 pt2 *. by elim/(TaggedP T2): _ / y => ? /f_inj->; apply/andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)