proposition: Lemma bunion_inter_compat_r s r rr : bunion s (fun x => rr x ∩ r) ≡ bunion s rr ∩ r.
proof: Proof. uu; split; ins; desf; eauto 8. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets