proposition: Lemma in_imfset2 (T1 : choiceType) (T2 : T1 -> choiceType) (f : forall x, T2 x -> K) (p1 : finmempred T1) (p2 : forall x, finmempred (T2 x)) (x : T1) (y : T2 x) : in_mem x p1 -> in_mem y (p2 x) -> f x y \in imfset2 key f p1 p2.
proof: Proof. by move=> xD1 yD2; apply/imfset2P; exists x => //; exists y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)