proposition: Lemma set_bunion_union_r s ss ss' : set_bunion s (fun 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