proposition: Lemma s2fU n (s1 s2 : {set 'I_n}) : s2f (s1 :|: s2) = s2f s1 `|` s2f s2.
proof: Proof. apply/fsetP => j; rewrite !inE. apply/imfsetP/orP => /= [[k]|[] /imfsetP[/= k]]. - by rewrite !inE -!mem_s2f => /orP[] kIs ->; [left|right]. - by move => kIs1 ->; exists k; rewrite // inE kIs1. by move => kIs2 ->; exists k; rewrite // inE kIs2 orbT. Qed.
imports: mathcomp(all_ssreflect finmap)