proposition: Lemma doubleton_in_Vomega x y (V := universe omega0): inc x V -> inc y V -> inc (doubleton x y) V.
proof: Proof. move => xv yv;apply:universe_omega_hi; first by apply: set2_finite. by move => t/set2_P; case => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)