[GOAL]
⊢ ¬UnivLE.{u + 1, u}
[PROOFSTEP]
simp only [Small_iff, not_forall, not_exists, not_nonempty_iff]
[GOAL]
⊢ ∃ x, ∀ (x_1 : Type u), IsEmpty (x ≃ x_1)
[PROOFSTEP]
exact ⟨Type u, fun α => ⟨fun f => Function.not_surjective_Type.{u, u} f.symm f.symm.surjective⟩⟩
