proposition: Lemma set_bunion_bunion_l s ss (ss' : B -> C -> Prop) : (⋃₁x ∈ (⋃₁y ∈ s, ss y), ss' x) ≡₁ ⋃₁y ∈ s, ⋃₁x ∈ ss y, ss' x.
proof: Proof. u. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms