proposition: Lemma up2_fnats x : natp x -> x <> \0c -> f (singleton x) = x.
proof: Proof. move => pa pb; have pc: ~(inc (singleton x) Nat /\ singleton x <> \0c). move => [ sa _]. move: (card_nat sa); rewrite cardinal_set1 => /set1_inj ex. by case: pb. have pd:(exists y, [/\ inc y Nat, y <> \0c & singleton x = singleton y]). exists x; split => //. by rewrite /f /universe_permutation_fun; Ytac0; Ytac0; rewrite setU_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)