diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 5f38f7974e..23abdcd1c9 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1138,7 +1138,7 @@ private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do
       pure LBool.true
     else
       unfold t
-       (unfold s (pure LBool.false) (fun s => isDefEqRight fn t s))
+       (unfold s (pure LBool.undef) (fun s => isDefEqRight fn t s))
        (fun t => unfold s (isDefEqLeft fn t s) (fun s => isDefEqLeftRight fn t s))
   | _, _ => pure LBool.false
 
diff --git a/tests/lean/run/interp.lean b/tests/lean/run/interp.lean
index 07af2131b3..e2cd73a612 100644
--- a/tests/lean/run/interp.lean
+++ b/tests/lean/run/interp.lean
@@ -9,7 +9,7 @@ inductive Ty where
   | bool
   | fn (a r : Ty)
 
-@[reducible] def Ty.interp : Ty → Type
+abbrev Ty.interp : Ty → Type
   | int    => Int
   | bool   => Bool
   | fn a r => a.interp → r.interp