proposition: Lemma pair_in_Vomega x y (V := universe omega0): inc x V -> inc y V -> inc (J x y) V.
proof: Proof. move => xv yv; rewrite kpairE. by apply: doubleton_in_Vomega;apply: doubleton_in_Vomega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)