proposition: Lemma set_disjoint_subset s s' (SUB: s ⊆₁ s') sr sr' (SUB': sr ⊆₁ sr') : set_disjoint s' sr' -> set_disjoint s sr.
proof: Proof. u. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms