proposition: Lemma set2_pr a b X: inc a X -> inc b X -> (forall z, inc z X -> z = a \/ z = b) -> X = doubleton a b.
proof: Proof. move => ax bx h; set_extens t; first by move => ta; apply /set2_P /h. by case /set2_P => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)