diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean
new file mode 100644
index 0000000000..7268fa8520
--- /dev/null
+++ b/src/Init/Grind/Util.lean
@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+
+namespace Lean.Grind
+
+/-- A helper gadget for annotating nested proofs in goals. -/
+def nestedProof (p : Prop) (h : p) : p := h
+
+end Lean.Grind
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 71ef14f4d0..41f47d18ea 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -167,7 +167,7 @@ def isDefEqStringLit (s t : Expr) : MetaM LBool := do
   Remark: `n` may be 0. -/
 def isEtaUnassignedMVar (e : Expr) : MetaM Bool := do
   match e.etaExpanded? with
-  | some (Expr.mvar mvarId) =>
+  | some (.mvar mvarId) =>
     if (← mvarId.isReadOnlyOrSyntheticOpaque) then
       pure false
     else if (← mvarId.isAssigned) then
@@ -361,9 +361,9 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
     let fvars  := fvars.push (mkFVar fvarId)
     isDefEqBindingAux lctx fvars b₁ b₂ (ds₂.push d₂)
   match e₁, e₂ with
-  | Expr.forallE n d₁ b₁ _, Expr.forallE _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
-  | Expr.lam     n d₁ b₁ _, Expr.lam     _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
-  | _,                      _                      =>
+  | .forallE n d₁ b₁ _, .forallE _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
+  | .lam     n d₁ b₁ _, .lam     _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
+  | _,                  _                  =>
     withLCtx' lctx do
       isDefEqBindingDomain fvars ds₂ do
         Meta.isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars)
@@ -1037,13 +1037,13 @@ def checkedAssignImpl (mvarId : MVarId) (val : Expr) : MetaM Bool := do
 
 private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
   match v with
-  | .mdata _ e   => processAssignmentFOApproxAux mvar args e
-  | Expr.app f a =>
+  | .mdata _ e => processAssignmentFOApproxAux mvar args e
+  | .app f a   =>
     if args.isEmpty then
       pure false
     else
       Meta.isExprDefEqAux args.back! a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
-  | _            => pure false
+  | _ => pure false
 
 /--
   Auxiliary method for applying first-order unification. It is an approximation.
@@ -1177,7 +1177,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
         let arg ← simpAssignmentArg arg
         let args := args.set i arg
         match arg with
-        | Expr.fvar fvarId =>
+        | .fvar fvarId =>
           if args[0:i].any fun prevArg => prevArg == arg then
             useFOApprox args
           else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then
@@ -1233,7 +1233,7 @@ private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do
 
 private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) := do
   match t.getAppFn with
-  | Expr.const c _ =>
+  | .const c _ =>
     match (← getUnfoldableConst? c) with
     | r@(some info) => if info.hasValue then return r else return none
     | _             => return none
@@ -1375,8 +1375,8 @@ private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do
 
 private def sameHeadSymbol (t s : Expr) : Bool :=
   match t.getAppFn, s.getAppFn with
-  | Expr.const c₁ _, Expr.const c₂ _ => c₁ == c₂
-  | _,               _               => false
+  | .const c₁ _, .const c₂ _ => c₁ == c₂
+  | _,           _           => false
 
 /--
   - If headSymbol (unfold t) == headSymbol s, then unfold t
@@ -1521,8 +1521,8 @@ private def isDefEqDelta (t s : Expr) : MetaM LBool := do
       unfoldNonProjFnDefEq tInfo sInfo t s
 
 private def isAssigned : Expr → MetaM Bool
-  | Expr.mvar mvarId => mvarId.isAssigned
-  | _                => pure false
+  | .mvar mvarId => mvarId.isAssigned
+  | _            => pure false
 
 private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
   let tFn := t.getAppFn
@@ -1647,8 +1647,8 @@ private partial def isDefEqQuick (t s : Expr) : MetaM LBool :=
   | .sort u,       .sort v     => toLBoolM <| isLevelDefEqAux u v
   | .lam ..,       .lam ..     => if t == s then pure LBool.true else toLBoolM <| isDefEqBinding t s
   | .forallE ..,   .forallE .. => if t == s then pure LBool.true else toLBoolM <| isDefEqBinding t s
-  -- | Expr.mdata _ t _,    s                   => isDefEqQuick t s
-  -- | t,                   Expr.mdata _ s _    => isDefEqQuick t s
+  -- | .mdata _ t _, s               => isDefEqQuick t s
+  -- | t,            .mdata _ s _    => isDefEqQuick t s
   | .fvar fvarId₁, .fvar fvarId₂ => do
     if fvarId₁ == fvarId₂ then
       return .true
diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index eb330d1428..d2c7fa1f09 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
 import Lean.Meta.Tactic.Grind.Canon
+import Lean.Meta.Tactic.Grind.MarkNestedProofs
 
 namespace Lean
 
@@ -22,5 +23,6 @@ builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.add
 builtin_initialize registerTraceClass `grind.pre
 builtin_initialize registerTraceClass `grind.debug
+builtin_initialize registerTraceClass `grind.congr
 
 end Lean
diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean
index 89df6f4df4..ceb1530594 100644
--- a/src/Lean/Meta/Tactic/Grind/Canon.lean
+++ b/src/Lean/Meta/Tactic/Grind/Canon.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Grind.Util
 import Lean.Meta.Basic
 import Lean.Meta.FunInfo
 import Lean.Util.FVarSubset
@@ -18,10 +19,8 @@ A canonicalizer module for the `grind` tactic. The canonicalizer defined in `Met
 not suitable for the `grind` tactic. It was designed for tactics such as `omega`, where the goal is
 to detect when two structurally different atoms are definitionally equal.
 
-The `grind` tactic, on the other hand, uses congruence closure but disregards types, type formers, instances, and proofs.
-Proofs are ignored due to proof irrelevance. Types, type formers, and instances are considered supporting
-elements and are not factored into congruence detection. Instead, `grind` only checks whether
-elements are structurally equal, which, in the context of the `grind` tactic, is equivalent to pointer equality.
+The `grind` tactic, on the other hand, uses congruence closure. Moreover, types, type formers, proofs, and instances
+are considered supporting elements and are not factored into congruence detection.
 
 This module minimizes the number of `isDefEq` checks by comparing two terms `a` and `b` only if they instances,
 types, or type formers and are the `i`-th arguments of two different `f`-applications. This approach is
@@ -31,6 +30,14 @@ To further optimize `isDefEq` checks, instances are compared using `Transparency
 the number of constants that need to be unfolded. If diagnostics are enabled, instances are compared using
 the default transparency mode too for sanity checking, and discrepancies are reported.
 Types and type formers are always checked using default transparency.
+
+Remark:
+The canonicalizer minimizes issues with non-canonical instances and structurally different but definitionally equal types,
+but it does not solve all problems. For example, consider a situation where we have `(a : BitVec n)`
+and `(b : BitVec m)`, along with instances `inst1 n : Add (BitVec n)` and `inst2 m : Add (BitVec m)` where `inst1`
+and `inst2` are structurally different. Now consider the terms `a + a` and `b + b`. After canonicalization, the two
+additions will still use structurally different (and definitionally different) instances: `inst1 n` and `inst2 m`.
+Furthermore, `grind` will not be able to infer that  `HEq (a + a) (b + b)` even if we add the assumptions `n = m` and `HEq a b`.
 -/
 
 structure State where
@@ -72,11 +79,6 @@ abbrev canonInst (f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <|
 Return type for the `shouldCanon` function.
 -/
 private inductive ShouldCanonResult where
-  | /-
-    Nested proofs are ignored by the canonizer.
-    That is, they are not canonized or recursively visited.
-    -/
-    ignore
   | /- Nested types (and type formers) are canonicalized. -/
     canonType
   | /- Nested instances are canonicalized. -/
@@ -97,7 +99,7 @@ def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Should
     if pinfo.isInstImplicit then
       return .canonInst
     else if pinfo.isProp then
-      return .ignore
+      return .visit
   if (← isTypeFormer arg) then
     return .canonType
   else
@@ -122,20 +124,25 @@ where
       if let some r := (← get).find? e then
         return r
       e.withApp fun f args => do
-        let pinfos := (← getFunInfo f).paramInfo
-        let mut modified := false
-        let mut args := args
-        for i in [:args.size] do
-          let arg := args[i]!
-          let arg' ← match (← shouldCanon pinfos i arg) with
-          | .ignore    => pure arg
-          | .canonType => canonType f i arg
-          | .canonInst => canonInst f i arg
-          | .visit     => visit arg
-          unless ptrEq arg arg' do
-            args := args.set! i arg'
-            modified := true
-        let e' := if modified then mkAppN f args else e
+        let e' ← if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
+          -- We just canonize the proposition
+          let prop := args[0]!
+          let prop' ← visit prop
+          pure <| if ptrEq prop prop' then mkAppN f (args.set! 0 prop') else e
+        else
+          let pinfos := (← getFunInfo f).paramInfo
+          let mut modified := false
+          let mut args := args
+          for i in [:args.size] do
+            let arg := args[i]!
+            let arg' ← match (← shouldCanon pinfos i arg) with
+            | .canonType  => canonType f i arg
+            | .canonInst  => canonInst f i arg
+            | .visit      => visit arg
+            unless ptrEq arg arg' do
+              args := args.set! i arg'
+              modified := true
+          pure <| if modified then mkAppN f args else e
         modify fun s => s.insert e e'
         return e'
 
diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean
index 81cbb6e164..ca69c22da5 100644
--- a/src/Lean/Meta/Tactic/Grind/Core.lean
+++ b/src/Lean/Meta/Tactic/Grind/Core.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Grind.Util
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.LitValues
 
@@ -28,7 +29,8 @@ where
 /-- Returns all equivalence classes in the current goal. -/
 partial def getEqcs : GoalM (List (List Expr)) := do
   let mut r := []
-  for (_, node) in (← get).enodes do
+  let nodes ← getENodes
+  for node in nodes do
     if isSameExpr node.root node.self then
       r := (← getEqc node.self) :: r
   return r
@@ -63,8 +65,7 @@ def ppENodeDecl (e : Expr) : GoalM Format := do
 /-- Pretty print goal state for debugging purposes. -/
 def ppState : GoalM Format := do
   let mut r := f!"Goal:"
-  let nodes := (← get).enodes.toArray.map (·.2)
-  let nodes := nodes.qsort fun a b => a.idx < b.idx
+  let nodes ← getENodes
   for node in nodes do
     r := r ++ "\n" ++ (← ppENodeDecl node.self)
   let eqcs ← getEqcs
@@ -94,18 +95,24 @@ def mkENode (e : Expr) (generation : Nat) : GoalM Unit := do
 private def pushNewEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit :=
   modify fun s => { s with newEqs := s.newEqs.push { lhs, rhs, proof, isHEq } }
 
-@[inline] private def pushNewEq (lhs rhs proof : Expr) : GoalM Unit :=
-  pushNewEqCore lhs rhs proof (isHEq := false)
+@[inline] private def pushNewEq (lhs rhs proof : Expr) : GoalM Unit := do
+  if (← isDefEq (← inferType lhs) (← inferType rhs)) then
+    pushNewEqCore lhs rhs proof (isHEq := false)
+  else
+    pushNewEqCore lhs rhs proof (isHEq := true)
 
-@[inline] private def pushNewHEq (lhs rhs proof : Expr) : GoalM Unit :=
-  pushNewEqCore lhs rhs proof (isHEq := true)
+/-- We use this auxiliary constant to mark delayed congruence proofs. -/
+private def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
 
-/--
-Adds `e` to congruence table.
--/
-def addCongrTable (_e : Expr) : GoalM Unit := do
-  -- TODO
-  return ()
+/-- Adds `e` to congruence table. -/
+def addCongrTable (e : Expr) : GoalM Unit := do
+  if let some { e := e' } := (← get).congrTable.find? { e } then
+    trace[grind.congr] "{e} = {e'}"
+    pushNewEq e e' congrPlaceholderProof
+    -- TODO: we must check whether the types of the functions are the same
+    -- TODO: update cgRoot for `e`
+  else
+    modify fun s => { s with congrTable := s.congrTable.insert { e } }
 
 partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
   if (← alreadyInternalized e) then return ()
@@ -126,20 +133,16 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
       -- We do not want to internalize the components of a literal value.
       mkENode e generation
     else e.withApp fun f args => do
-      unless f.isConst do
-        internalize f generation
-      let info ← getFunInfo f
-      let shouldInternalize (i : Nat) : GoalM Bool := do
-        if h : i < info.paramInfo.size then
-          let pinfo := info.paramInfo[i]
-          if pinfo.binderInfo.isInstImplicit || pinfo.isProp then
-            return false
-        return true
-      for h : i in [: args.size] do
-        let arg := args[i]
-        if (← shouldInternalize i) then
-          unless (← isTypeFormer arg) do
-            internalize arg generation
+      if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
+        -- We only internalize the proposition. We can skip the proof because of
+        -- proof irrelevance
+        internalize args[0]! generation
+      else
+        unless f.isConst do
+          internalize f generation
+        for h : i in [: args.size] do
+          let arg := args[i]
+          internalize arg generation
       mkENode e generation
       addCongrTable e
 
@@ -237,10 +240,17 @@ where
     loop lhs
 
 /-- Ensures collection of equations to be processed is empty. -/
-def resetNewEqs : GoalM Unit :=
+private def resetNewEqs : GoalM Unit :=
   modify fun s => { s with newEqs := #[] }
 
-partial def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
+/-- Pops and returns the next equality to be processed. -/
+private def popNextEq? : GoalM (Option NewEq) := do
+  let r := (← get).newEqs.back?
+  if r.isSome then
+    modify fun s => { s with newEqs := s.newEqs.pop }
+  return r
+
+private partial def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
   addEqStep lhs rhs proof isHEq
   processTodo
 where
@@ -248,7 +258,7 @@ where
     if (← isInconsistent) then
       resetNewEqs
       return ()
-    let some { lhs, rhs, proof, isHEq } := (← get).newEqs.back? | return ()
+    let some { lhs, rhs, proof, isHEq } := (← popNextEq?) | return ()
     addEqStep lhs rhs proof isHEq
     processTodo
 
@@ -273,7 +283,7 @@ where
     trace[grind.add] "isNeg: {isNeg}, {p}"
     match_expr p with
     | Eq _ lhs rhs => goEq p lhs rhs isNeg false
-    | HEq _ _ lhs rhs => goEq p lhs rhs isNeg true
+    | HEq _ lhs _ rhs => goEq p lhs rhs isNeg true
     | _ =>
       internalize p generation
       if isNeg then
diff --git a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
new file mode 100644
index 0000000000..600847671d
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Util
+import Lean.Util.PtrSet
+import Lean.Meta.Basic
+import Lean.Meta.InferType
+
+namespace Lean.Meta.Grind
+
+unsafe def markNestedProofsImpl (e : Expr) : MetaM Expr := do
+  visit e |>.run' mkPtrMap
+where
+  visit (e : Expr) : StateRefT (PtrMap Expr Expr) MetaM Expr := do
+    if (← isProof e) then
+      if e.isAppOf ``Lean.Grind.nestedProof then
+        return e -- `e` is already marked
+      if let some r := (← get).find? e then
+        return r
+      let prop ← inferType e
+      let e' := mkApp2 (mkConst ``Lean.Grind.nestedProof) prop e
+      modify fun s => s.insert e e'
+      return e'
+    else match e with
+      | .bvar .. => unreachable!
+      -- See comments on `Canon.lean` for why we do not visit these cases.
+      | .letE .. | .forallE .. | .lam ..
+      | .const .. | .lit .. | .mvar .. | .sort .. | .fvar ..
+      | .proj ..
+      | .mdata ..  => return e
+      -- We only visit applications
+      | .app .. =>
+        -- Check whether it is cached
+        if let some r := (← get).find? e then
+          return r
+        e.withApp fun f args => do
+          let mut modified := false
+          let mut args := args
+          for i in [:args.size] do
+            let arg := args[i]!
+            let arg' ← visit arg
+            unless ptrEq arg arg' do
+              args := args.set! i arg'
+              modified := true
+          let e' := if modified then mkAppN f args else e
+          modify fun s => s.insert e e'
+          return e'
+
+/--
+Wrap nested proofs `e` with `Lean.Grind.nestedProof`-applications.
+Recall that the congruence closure module has special support for `Lean.Grind.nestedProof`.
+-/
+def markNestedProofs (e : Expr) : MetaM Expr :=
+  unsafe markNestedProofsImpl e
+
+end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Preprocessor.lean b/src/Lean/Meta/Tactic/Grind/Preprocessor.lean
index 7fe08ea5d4..024df33fcd 100644
--- a/src/Lean/Meta/Tactic/Grind/Preprocessor.lean
+++ b/src/Lean/Meta/Tactic/Grind/Preprocessor.lean
@@ -16,6 +16,7 @@ import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
+import Lean.Meta.Tactic.Grind.MarkNestedProofs
 
 namespace Lean.Meta.Grind
 namespace Preprocessor
@@ -71,6 +72,8 @@ def introNext (goal : Goal) : PreM IntroResult := do
         -- TODO: keep applying simp/eraseIrrelevantMData/canon/shareCommon until no progress
         let r ← simp goal p
         let p' := r.expr
+        let p' ← markNestedProofs p'
+        let p' ← unfoldReducible p'
         let p' ← eraseIrrelevantMData p'
         let p' ← foldProjs p'
         let p' ← normalizeLevels p'
@@ -97,7 +100,7 @@ def introNext (goal : Goal) : PreM IntroResult := do
       let localDecl ← fvarId.getDecl
       if (← isProp localDecl.type) then
         -- Add a non-dependent copy
-        let mvarId ← mvarId.assert localDecl.userName localDecl.type (mkFVar fvarId)
+        let mvarId ← mvarId.assert (← mkFreshUserName localDecl.userName) localDecl.type (mkFVar fvarId)
         return .newDepHyp { goal with mvarId }
       else
         return .newLocal fvarId { goal with mvarId }
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 640a290171..30263d1f49 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -160,9 +160,68 @@ structure NewEq where
   proof : Expr
   isHEq : Bool
 
+abbrev ENodes := PHashMap USize ENode
+
+structure CongrKey (enodes : ENodes) where
+  e : Expr
+
+private abbrev toENodeKey (e : Expr) : USize :=
+  unsafe ptrAddrUnsafe e
+
+private def hashRoot (enodes : ENodes) (e : Expr) : UInt64 :=
+  if let some node := enodes.find? (toENodeKey e) then
+    toENodeKey node.root |>.toUInt64
+  else
+    13
+
+private def hasSameRoot (enodes : ENodes) (a b : Expr) : Bool := Id.run do
+  let ka := toENodeKey a
+  let kb := toENodeKey b
+  if ka == kb then
+    return true
+  else
+    let some n1 := enodes.find? ka | return false
+    let some n2 := enodes.find? kb | return false
+    toENodeKey n1.root == toENodeKey n2.root
+
+def congrHash (enodes : ENodes) (e : Expr) : UInt64 :=
+  if e.isAppOfArity ``Lean.Grind.nestedProof 2 then
+    -- We only hash the proposition
+    hashRoot enodes (e.getArg! 0)
+  else
+    go e 17
+where
+  go (e : Expr) (r : UInt64) : UInt64 :=
+    match e with
+    | .app f a => go f (mixHash r (hashRoot enodes a))
+    | _ => mixHash r (hashRoot enodes e)
+
+partial def isCongruent (enodes : ENodes) (a b : Expr) : Bool :=
+  if a.isAppOfArity ``Lean.Grind.nestedProof 2 && b.isAppOfArity ``Lean.Grind.nestedProof 2 then
+    hasSameRoot enodes (a.getArg! 0) (b.getArg! 0)
+  else
+    go a b
+where
+  go (a b : Expr) : Bool :=
+    if a.isApp && b.isApp then
+      hasSameRoot enodes a.appArg! b.appArg! && go a.appFn! b.appFn!
+    else
+      -- Remark: we do not check whether the types of the functions are equal here
+      -- because we are not in the `MetaM` monad.
+      hasSameRoot enodes a b
+
+instance : Hashable (CongrKey enodes) where
+  hash k := congrHash enodes k.e
+
+instance : BEq (CongrKey enodes) where
+  beq k1 k2 := isCongruent enodes k1.e k2.e
+
+abbrev CongrTable (enodes : ENodes) := PHashSet (CongrKey enodes)
+
 structure Goal where
   mvarId       : MVarId
-  enodes       : PHashMap USize ENode := {}
+  enodes       : ENodes := {}
+  congrTable   : CongrTable enodes := {}
   /-- Equations to be processed. -/
   newEqs       : Array NewEq := #[]
   /-- `inconsistent := true` if `ENode`s for `True` and `False` are in the same equivalence class. -/
@@ -209,7 +268,10 @@ def alreadyInternalized (e : Expr) : GoalM Bool :=
   return (← get).enodes.contains (unsafe ptrAddrUnsafe e)
 
 def setENode (e : Expr) (n : ENode) : GoalM Unit :=
-  modify fun s => { s with enodes := s.enodes.insert (unsafe ptrAddrUnsafe e) n }
+  modify fun s => { s with
+    enodes := s.enodes.insert (unsafe ptrAddrUnsafe e) n
+    congrTable := unsafe unsafeCast s.congrTable
+  }
 
 def mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) : GoalM Unit := do
   setENode e {
@@ -230,10 +292,14 @@ def mkGoal (mvarId : MVarId) : GrindM Goal := do
     mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0)
     mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0)
 
-def forEachENode (f : ENode → GoalM Unit) : GoalM Unit := do
-  -- We must sort because we are using pointer addresses to hash
+/-- Returns all enodes in the goal -/
+def getENodes : GoalM (Array ENode) := do
+  -- We must sort because we are using pointer addresses as keys in `enodes`
   let nodes := (← get).enodes.toArray.map (·.2)
-  let nodes := nodes.qsort fun a b => a.idx < b.idx
+  return nodes.qsort fun a b => a.idx < b.idx
+
+def forEachENode (f : ENode → GoalM Unit) : GoalM Unit := do
+  let nodes ← getENodes
   for n in nodes do
     f n
 
diff --git a/tests/lean/run/grind_congr.lean b/tests/lean/run/grind_congr.lean
new file mode 100644
index 0000000000..7b12852b57
--- /dev/null
+++ b/tests/lean/run/grind_congr.lean
@@ -0,0 +1,22 @@
+import Lean
+
+def f (a : Nat) := a + a + a
+
+-- Prints the equivalence class containing a `f` application
+open Lean Meta Elab Tactic Grind in
+elab "grind_test" : tactic => withMainContext do
+  let declName := (← Term.getDeclName?).getD `_main
+  Meta.Grind.preprocessAndProbe (← getMainGoal) declName do
+    let #[n, _] ← filterENodes fun e => return e.self.isAppOf ``f | unreachable!
+    let eqc ← getEqc n.self
+    logInfo eqc
+
+/--
+info: [d, f b, c, f a]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (a b c d : Nat) : a = b → f a = c → f b = d → False := by
+  grind_test
+  sorry
diff --git a/tests/lean/run/grind_nested_proofs.lean b/tests/lean/run/grind_nested_proofs.lean
new file mode 100644
index 0000000000..6262d42952
--- /dev/null
+++ b/tests/lean/run/grind_nested_proofs.lean
@@ -0,0 +1,22 @@
+import Lean
+
+def f (α : Type) [Add α] (a : α) := a + a + a
+
+open Lean Meta Elab Tactic Grind in
+elab "grind_test" : tactic => withMainContext do
+  let declName := (← Term.getDeclName?).getD `_main
+  Meta.Grind.preprocessAndProbe (← getMainGoal) declName do
+    let nodes ← filterENodes fun e => return e.self.isAppOf ``Lean.Grind.nestedProof
+    logInfo (nodes.toList.map (·.self))
+
+/--
+info: [Lean.Grind.nestedProof (i < a.toList.length) (_example.proof_1 i j a b h1 h2),
+ Lean.Grind.nestedProof (j < a.toList.length) h1,
+ Lean.Grind.nestedProof (j < b.toList.length) h]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i ≤ j) : a[i] < a[j] + b[j] → i = j → a = b → False := by
+  grind_test
+  sorry
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index 22d4ff298d..456a05d21d 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -77,7 +77,6 @@ def g (i : Nat) (j : Nat) (_ : i > j := by omega) := i + j
 
 example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by
   grind_pre
-  guard_hyp h : j + 1 ≤ i
   next hn =>
   guard_hyp hn : ¬g (i + 1) j _ = i + j + 1
   simp_arith [g] at hn