proposition: Lemma set_equiv_bunion s s' (S: s ≡₁ s') ss ss' (SS: forall x (COND: s x), ss x ≡₁ ss' x) : set_bunion s ss ≡₁ set_bunion s' ss'.
proof: Proof. u. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms