proposition: Lemma s2f1 n (i : 'I_n) : s2f [set i] = [fset (nat_of_ord i)].
proof: Proof. apply/fsetP => j; rewrite !inE. apply/imfsetP/eqP => /= [[k]|->]; first by rewrite inE => /eqP ->. by exists i; rewrite ?inE. Qed.
imports: mathcomp(all_ssreflect finmap)