diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index d49738bac8..dc4f4e5d37 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -213,7 +213,8 @@ private def Config.toKey (c : Config) : UInt64 :=
   (c.univApprox.toUInt64 <<< 16) |||
   (c.etaStruct.toUInt64 <<< 17) |||
   (c.proj.toUInt64 <<< 19) |||
-  (c.zetaHave.toUInt64 <<< 21)
+  (c.zetaHave.toUInt64 <<< 21) |||
+  (c.zetaUnused.toUInt64 <<< 22)
 
 /-- Configuration with key produced by `Config.toKey`. -/
 structure ConfigWithKey where
diff --git a/tests/elab/13770.lean b/tests/elab/13770.lean
new file mode 100644
index 0000000000..3bbf3ee176
--- /dev/null
+++ b/tests/elab/13770.lean
@@ -0,0 +1,16 @@
+module
+
+import Lean
+
+/-!
+Regression test for https://github.com/leanprover/lean4/issues/13770.
+
+`Meta.Config.zetaUnused` controls `whnfCore`/`isDefEqQuick` reduction of unused `let`/`have`
+bindings, so two configs differing only in `zetaUnused` must produce distinct cache keys.
+-/
+
+open Lean Meta
+
+#guard
+  ({ zetaUnused := false } : Meta.Config).toConfigWithKey.key !=
+  ({ zetaUnused := true  } : Meta.Config).toConfigWithKey.key