proposition: Lemma set_subset_bunion s s' (S: s ⊆₁ s') ss ss' (SS: forall x (COND: s x), ss x ⊆₁ ss' x) : (⋃₁x ∈ s, ss x) ⊆₁ ⋃₁x ∈ s, ss' x.
proof: Proof. u. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms