diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
index fe47a0e..9d0e69b 100644
--- a/Auto/Translation/Monomorphization.lean
+++ b/Auto/Translation/Monomorphization.lean
@@ -620,12 +620,15 @@ def termLikeDefEqDefEqs (lemmas : Array Lemma) : MetaM (Array Lemma) := do
         if let .ok (.some (proof, eq, params)) ← computation then
           let eq := Expr.eraseMData (← Core.betaReduce eq)
           let eq ← Meta.transform eq (pre := fun e => do return .continue (← unfoldProj e))
-          let_expr Eq _ lhs rhs := eq | continue
-          if lhs == rhs then
+          if ← isTrivialEq eq then
             continue
           trace[auto.mono.termLikeDefEq] "{eq}"
           ret := ret.push ⟨⟨proof, eq, .leaf "termLikeDefEq"⟩, params⟩
   return ret
+where
+  isTrivialEq (e : Expr) : MetaM Bool := Meta.forallTelescope e fun _ b => do
+    let_expr Eq _ lhs rhs := b | return false
+    return lhs == rhs
 
 def initializeMonoM (lemmas : Array Lemma) : MonoM Unit := do
   let lemmas := lemmas ++ (← termLikeDefEqDefEqs lemmas)