proposition: Lemma Eq_set2_C2 x y: x <> y -> doubleton x y \Eq C2.
proof: Proof. move => h; move:(set2_equipotent_aux h); set g := Lf _ _ _. move =>[gp _ _]. apply: (equipotent_bp gp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)