diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index d754768fd893..f21de383530b 100644
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -303,9 +303,13 @@ theorem exists_or : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x :=
 
 @[simp] theorem exists_false : ¬(∃ _a : α, False) := fun ⟨_, h⟩ => h
 
-@[simp] theorem forall_const (α : Sort _) [i : Nonempty α] : (α → b) ↔ b :=
+-- This is not a good simp lemma, as it applies to any arrow, and generates a `Nonempty` side goal.
+theorem forall_const (α : Sort _) [i : Nonempty α] : (α → b) ↔ b :=
   ⟨i.elim, fun hb _ => hb⟩
 
+@[simp] theorem not_forall_of_nonempty [Nonempty β] : ((α → β) → False) ↔ False := by
+  simp [forall_const]
+
 theorem Exists.nonempty : (∃ x, p x) → Nonempty α | ⟨x, _⟩ => ⟨x⟩
 
 theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, p x