proposition: Lemma set_disjoint_bunion_r s ss sr : set_disjoint sr (set_bunion s ss) <-> forall x (IN: s x), set_disjoint sr (ss x).
proof: Proof. u. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms