proposition: Lemma up2_fperm x : f (f x) = x.
proof: Proof. case: (equal_or_not x \0c) => xz; first by rewrite xz up2_f0 up2_f0. case: (inc_or_not x Nat) => xN. by rewrite (up2_fnat xN xz); apply: up2_fnats. have pa: ~ (inc x Nat /\ x <> \0c) by move => []. case: (p_or_not_p (exists y, [/\ inc y Nat, y <> \0c & x = singleton y]))=> h. move:h => [y [yn tnz yv]]; rewrite yv up2_fnats // up2_fnat //. suff fx: f x = x by rewrite fx. by rewrite /f /universe_permutation_fun; Ytac0; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)