proposition: Lemma pr1_pair x y: P (J x y) = x.
proof: Proof. rewrite kpr1E kpairE -{2} (setU_1 x); congr union. have sx_k: inc (singleton x) (kpair_def x y) by apply: set2_1. apply: set1_pr. apply: setI_i;first by exists (singleton x). move => z /set2_P [] ->; fprops. move=> z zi; apply/set1_P; apply: (setI_hi zi sx_k). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)