proposition: Lemma set_of_card_oneP x: cardinal x = \1c <-> singletonp x.
proof: Proof. split; last by move => [y ->]; apply:cardinal_set1. move/esym; rewrite -(card_card CS1); move /card_eqP; rewrite /card_one. move=> [f [[[ff injf] sf] srf <-]]; exists (Vf f emptyset). apply: set1_pr; first by Wtac; rewrite srf;fprops. move => z /(proj2 sf) [y]; rewrite srf; move=> /set1_P -> <-; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)