theorem Set.subset_empty_iff._simp_1
theorem Set.subset_empty_iff._simp_1
: ∀ {α : Type u} {s : zpg9xh52.Set α}, Subset s EmptyCollection.emptyCollection = (s = EmptyCollection.emptyCollection)