proposition: Lemma setX_P x A B: inc x (A \times B) <-> [/\ pairp x, inc (P x) A & inc (Q x) B].
proof: Proof. split. move/setU_P => [a xa /funI_P [t ty ft]]. move: xa; rewrite ft; move/funI_P => [u uz ->]; aw; split; fprops. move => [px Px Qx];apply/setU_P; exists (fun_image B (J (P x))); apply/funI_P; [ exists (Q x); fprops; aw | by exists (P x) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)