diff --git a/library/init/meta/smt/congruence_closure.lean b/library/init/meta/smt/congruence_closure.lean
index b4fd85c17f..6282452091 100644
--- a/library/init/meta/smt/congruence_closure.lean
+++ b/library/init/meta/smt/congruence_closure.lean
@@ -121,7 +121,6 @@ do (lhs, rhs) ← target >>= match_eq,
    s ← s^.internalize rhs,
    b ← s^.is_eqv lhs rhs,
    if b then do {
-     t ← return $ expr.const `true [],
      s^.eqv_proof lhs rhs >>= exact
    } else do {
      fail "ac_refl failed"