diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index c6ff4c05b2..896ef5306e 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -287,8 +287,9 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
   let rec go (mvarId : MVarId) : MetaM Unit := do
     if (← tryEqns mvarId) then
       return ()
-    else if let some mvarId ← funext? mvarId then
-      go mvarId
+    -- Remark: we removed funext? from `mkEqnTypes`
+    -- else if let some mvarId ← funext? mvarId then
+    --  go mvarId
     else if let some mvarId ← simpMatch? mvarId then
       go mvarId
     else if let some mvarIds ← splitTarget? mvarId (splitIte := false) then