proposition: Lemma up2_fnat x : natp x -> x <> \0c -> f x = singleton x.
proof: Proof. move => pa pb; move: (conj pa pb) => pc. by rewrite /f /universe_permutation_fun; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)