proposition: Lemma set_equiv_bunion_guard s s' (S: s ≡₁ s') ss ss' (EQ: ss = ss') : set_bunion s ss ≡₁ set_bunion s' ss'.
proof: Proof. subst; u. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms