proposition: Lemma s2f_setT n : s2f (setT : {set 'I_n}) = sint 0 n.
proof: Proof. apply/fsetP => i; rewrite mem_sint /=. apply/imfsetP/idP => /= [[j _ -> //]| iLn]. by exists (Ordinal iLn). Qed.
imports: mathcomp(all_ssreflect finmap)