proposition: Lemma restr_bunion A B (f : B -> Prop) (s: A -> Prop) rr : restr_rel f (⋃x ∈ s, rr x) ≡ ⋃x ∈ s, restr_rel f (rr x).
proof: Proof. u. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets