proposition: Lemma set_disjoint_union_l s s' s'' : set_disjoint (s ∪₁ s') s'' <-> set_disjoint s s'' /\ set_disjoint s' s''.
proof: Proof. u. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms