proposition: Lemma set_bunion_minus_compat_r s sb ss : set_bunion s (fun x => ss x \₁ sb) ≡₁ set_bunion s ss \₁ sb.
proof: Proof. u; split; ins; desf; eauto 8. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms