diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp
index d063052894..974a7517aa 100644
--- a/src/library/equations_compiler/elim_match.cpp
+++ b/src/library/equations_compiler/elim_match.cpp
@@ -331,7 +331,15 @@ struct elim_match_fn {
     expr whnf_pattern(type_context & ctx, expr const & e) {
         if (is_inaccessible(e)) {
             return e;
+        } else if (is_value(ctx, e)) {
+            return e;
         } else {
+            /* The case is_value(ctx, e) above is needed because whnf_head_pred does not check the given predicate
+               before unfolding projections. Moreover, some values are projections applications.
+               Example:
+                  (@has_zero.zero nat nat.has_zero)
+                  (@has_one.one nat nat.has_one)
+            */
             return ctx.whnf_head_pred(e, [&](expr const & e) {
                     return !is_constructor_app(ctx, e) && !is_value(ctx, e) && !is_transport_app(e);
                 });
diff --git a/tests/lean/run/eqn_value_issue.lean b/tests/lean/run/eqn_value_issue.lean
new file mode 100644
index 0000000000..9c4c49b506
--- /dev/null
+++ b/tests/lean/run/eqn_value_issue.lean
@@ -0,0 +1,17 @@
+def f : nat -> nat
+| 1    := 1
+| 2000 := 2
+| _    := 3
+
+#check f.equations._eqn_1
+#check f.equations._eqn_2
+#check f.equations._eqn_3
+
+def g : nat -> nat
+| 0    := 1
+| 2000 := 2
+| _    := 3
+
+#check g.equations._eqn_1
+#check g.equations._eqn_2
+#check g.equations._eqn_3