diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean
index fbb390dfdf..52fdd8ac2b 100644
--- a/src/Lean/Meta/Reduce.lean
+++ b/src/Lean/Meta/Reduce.lean
@@ -32,9 +32,10 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta
             else
               args ← args.modifyM i visit
           pure (mkAppN f args)
-        | Expr.lam ..     => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
-        | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
-        | _               => return e
+        | Expr.lam ..        => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
+        | Expr.forallE ..    => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
+        | Expr.proj n i s .. => return mkProj n i (← visit s)
+        | _                  => return e
   visit e |>.run
 
 end Lean.Meta
diff --git a/tests/lean/620.lean b/tests/lean/620.lean
new file mode 100644
index 0000000000..df4a5e6c69
--- /dev/null
+++ b/tests/lean/620.lean
@@ -0,0 +1,7 @@
+structure Foo (α : Type) where foo : α
+class Bar (α β : Type) where coe : α → β
+
+variable {α : Type} (x : Foo (Foo α))
+
+#reduce @Coe.coe (Foo (Foo α)) (Foo α) (Coe.mk fun y => y.foo) x -- x.1
+#reduce (@Coe.coe (Foo (Foo α)) (Foo α) (Coe.mk fun y => y.foo) x).1 -- (Coe.coe x).1 instead of x.1.1
diff --git a/tests/lean/620.lean.expected.out b/tests/lean/620.lean.expected.out
new file mode 100644
index 0000000000..1d64a03799
--- /dev/null
+++ b/tests/lean/620.lean.expected.out
@@ -0,0 +1,2 @@
+x.1
+x.1.1