proposition: Lemma s2f_pred n (s : {set 'I_n}) (P : pred nat) : s2f [set i in s | P i] = [fset i in (s2f s) | P i].
proof: Proof. apply/fsetP=> i; rewrite !inE /=. apply/imfsetP/andP => /= [[j]|]. rewrite !inE => /andP[jIs jP] ->; split => //. by apply/imfsetP; exists j. move=> [/imfsetP[/= j jIs ->] jP]; exists j => //. by rewrite inE jIs. Qed.
imports: mathcomp(all_ssreflect finmap)