proposition: Lemma mem_s2f n (s : {set 'I_n}) (i : 'I_n) : (i : nat) \in s2f s = (i \in s).
proof: Proof. apply/imfsetP/idP => /= [[j jIs iEj]|iIs]; last by exists i. by rewrite (_ : i = j) //; apply: val_inj. Qed.
imports: mathcomp(all_ssreflect finmap)