proposition: Lemma imfset2P (T1 : choiceType) (T2 : T1 -> choiceType) (f : forall x, T2 x -> K) (p1 : finmempred T1) (p2 : forall x, finmempred (T2 x)) k : reflect (exists2 x : T1, in_mem x p1 & exists2 y : T2 x, in_mem y (p2 x) & k = f x y) (k \in imfset2 key f p1 p2).
proof: Proof. rewrite unlock !seq_fsetE; apply: (iffP allpairsPdep). move=> [x [y]]; rewrite !enum_finmemE => -[xp yp ->]. by exists x => //; exists y. by move=> [x xp [y yp ->]]; exists x, y; rewrite ?enum_finmemE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)