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