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