diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index bc6a668a6b57..657543d536c5 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -569,12 +569,16 @@ def mkLetBodyCongr (a h : Expr) : MetaM Expr :=
   mkAppM ``let_body_congr #[a, h]
 
 /-- Return `of_eq_true h` -/
-def mkOfEqTrue (h : Expr) : MetaM Expr :=
-  mkAppM ``of_eq_true #[h]
+def mkOfEqTrue (h : Expr) : MetaM Expr := do
+  match_expr h with
+  | eq_true _ h => return h
+  | _ => mkAppM ``of_eq_true #[h]
 
 /-- Return `eq_true h` -/
-def mkEqTrue (h : Expr) : MetaM Expr :=
-  mkAppM ``eq_true #[h]
+def mkEqTrue (h : Expr) : MetaM Expr := do
+  match_expr h with
+  | of_eq_true _ h => return h
+  | _ => return mkApp2 (mkConst ``eq_true) (← inferType h) h
 
 /--
   Return `eq_false h`
diff --git a/tests/lean/run/grind_offset_cnstr.lean b/tests/lean/run/grind_offset_cnstr.lean
index 9b7e084372e6..9bf50577b9ff 100644
--- a/tests/lean/run/grind_offset_cnstr.lean
+++ b/tests/lean/run/grind_offset_cnstr.lean
@@ -160,3 +160,10 @@ example (a1 a2 a3 : Nat) :
         a1 ≤ a2 + 5 → a2 ≤ a3 + 2 → False := by
   fail_if_success grind
   sorry
+
+
+set_option trace.grind.debug.offset.proof true in
+example (a1 a2 a3 : Nat) :
+        a1 ≤ a2 + 5 → a2 ≤ a3 + 2 → False := by
+  fail_if_success grind
+  sorry