proposition: Lemma set2_equipotent_aux x y (g := (Lf (variant x C0 C1) (doubleton x y) C2)): x <> y -> [/\ bijection_prop g (doubleton x y) C2, Vf g x = C0 & Vf g y = C1].
proof: Proof. move => neq. have ax: lf_axiom (variant x C0 C1) (doubleton x y) C2. by rewrite /variant;move => t tp; apply /set2_P; Ytac h; [left | right]. rewrite ! LfV;fprops; rewrite /variant; Ytac0; Ytac0; split => //. rewrite /g/variant;saw;apply: lf_bijective => //. move=> u v /set2_P [] -> /set2_P [] -> //; Ytac0 => //; Ytac0 => // => h. - by case: C0_ne_C1. - by case: C1_ne_C0. by move => z; case/C2_P => ->; [exists x | exists y]; fprops; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)