small fix

arthur-adjedj · arthur-adjedj · commit b586ad1730a1 · 2026-02-26T12:30:39.000+01:00
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
@@ -2142,7 +2142,8 @@ private partial def isUnitLikeType (e : Expr) : MetaM Bool :=
 private def isDefEqUnitLike (t : Expr) (s : Expr) : MetaM Bool := do
   let tType  ← inferType t
     match (← cachedUnitLike? tType) with
-      | some b => return b
+      | some false => return false
+      | some true => Meta.isExprDefEqAux tType (← inferType s)
       | none => cacheUnitLike tType (← do
         let isUnit ← isUnitLikeType tType
         if !isUnit then return false
