proposition: Lemma bunion_union_r s rr rr' : bunion s (fun x => rr x ∪ rr' x) ≡ bunion s rr ∪ bunion s rr'.
proof: Proof. uu. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets