proposition: Lemma collect_rel_bunion f (s : C -> Prop) rr : f ↑ (⋃x ∈ s, rr x) ≡ ⋃x ∈ s, f ↑ (rr x).
proof: Proof. u; eauto 8. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets