diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index e245c8a890..6990bd85aa 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -14,6 +14,11 @@ import Lean.Meta.Match.Value
 namespace Lean.Meta
 namespace Simp
 
+register_builtin_option backward.dsimp.proofs : Bool := {
+    defValue := false
+    descr    := "Let `dsimp` simplify proof terms"
+  }
+
 builtin_initialize congrHypothesisExceptionId : InternalExceptionId ←
   registerInternalExceptionId `congrHypothesisFailed
 
@@ -423,6 +428,16 @@ private def dsimpReduce : DSimproc := fun e => do
     eNew ← reduceFVar (← getConfig) (← getSimpTheorems) eNew
   if eNew != e then return .visit eNew else return .done e
 
+/-- Auxiliary `dsimproc` for not visiting proof terms. -/
+private def doNotVisitProofs : DSimproc := fun e => do
+  if ← isProof e then
+    if !backward.dsimp.proofs.get (← getOptions) then
+      return .done e
+    else
+      return .continue e
+  else
+    return .continue e
+
 /-- Helper `dsimproc` for `doNotVisitOfNat` and `doNotVisitOfScientific` -/
 private def doNotVisit (pred : Expr → Bool) (declName : Name) : DSimproc := fun e => do
   if pred e then
@@ -459,7 +474,7 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   unless cfg.dsimp do
     return e
   let m ← getMethods
-  let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit
+  let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit >> doNotVisitProofs
   let post := m.dpost >> dsimpReduce
   withInDSimp do
   transform (usedLetOnly := cfg.zeta || cfg.zetaUnused) e (pre := pre) (post := post)
diff --git a/tests/lean/run/dsimp_proofs.lean b/tests/lean/run/dsimp_proofs.lean
new file mode 100644
index 0000000000..0b8ac52573
--- /dev/null
+++ b/tests/lean/run/dsimp_proofs.lean
@@ -0,0 +1,7 @@
+@[simp]
+theorem foo (i : Nonempty α) : Nonempty.intro (Classical.choice i) = i := rfl
+
+/-- error: dsimp made no progress -/
+#guard_msgs in
+example : Classical.choice (Nonempty.intro (Classical.choice instNonemptyFloat)) = 0 := by
+  dsimp