apply Set.ext
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
⊢ Set.map f Set.empty = Set.empty
case a
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
⊢ ∀ (x : β), x ∈ Set.map f Set.empty ↔ x ∈ Set.empty