proposition: Lemma s2fD n (s1 s2 : {set 'I_n}) : s2f (s1 :\: s2) = s2f s1 `\` s2f s2.
proof: Proof. apply/fsetP => j; rewrite !inE. apply/imfsetP/andP => /= [[k]|[jDi /imfsetP[/= k kIs jEk]]]. by rewrite !inE -!mem_s2f => /andP[kDi kIs] ->. by exists k => //; rewrite !inE kIs -mem_s2f -jEk jDi. Qed.
imports: mathcomp(all_ssreflect finmap)