diff --git a/src/Lean/Meta/Tactic/Grind/Inv.lean b/src/Lean/Meta/Tactic/Grind/Inv.lean
index 539924e850..c3fbd1f32f 100644
--- a/src/Lean/Meta/Tactic/Grind/Inv.lean
+++ b/src/Lean/Meta/Tactic/Grind/Inv.lean
@@ -63,32 +63,34 @@ def checkMatchCondParent (e : Expr) (parent : Expr) : GoalM Bool := do
   return false
 
 def checkParents (e : Expr) : GoalM Unit := do
-  -- **Note**: We currently do not check the `funCC` case
-  unless (← useFunCC e) do
-    if (← isRoot e) then
-      for parent in (← getParents e).elems do
-        if isMatchCond parent then
-          unless (← checkMatchCondParent e parent) do
+  -- **Note**: We skip `funCC` parents because the parent-child relationship uses
+  -- one-level decomposition (`appFn!`/`appArg!`) rather than full `getAppArgs`/`getAppFn`.
+  if (← isRoot e) then
+    for parent in (← getParents e).elems do
+      if parent.isApp && (← useFunCC parent) then
+        pure ()
+      else if isMatchCond parent then
+        unless (← checkMatchCondParent e parent) do
+          throwError "e: {e}, parent: {parent}"
+        assert! (← checkMatchCondParent e parent)
+      else
+        let mut found := false
+        -- There is an argument `arg` s.t. root of `arg` is `e`.
+        for arg in parent.getAppArgs do
+          if (← checkChild e arg) then
+            found := true
+            break
+        -- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`.
+        if let .forallE _ d b _ := parent then
+          if (← checkChild e d) then
+            found := true
+          unless b.hasLooseBVars do
+            if (← checkChild e b) then
+              found := true
+        unless found do
+          unless (← checkChild e parent.getAppFn) do
             throwError "e: {e}, parent: {parent}"
-          assert! (← checkMatchCondParent e parent)
-        else
-          let mut found := false
-          -- There is an argument `arg` s.t. root of `arg` is `e`.
-          for arg in parent.getAppArgs do
-            if (← checkChild e arg) then
-              found := true
-              break
-          -- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`.
-          if let .forallE _ d b _ := parent then
-            if (← checkChild e d) then
-              found := true
-            unless b.hasLooseBVars do
-              if (← checkChild e b) then
-                found := true
-          unless found do
-            unless (← checkChild e parent.getAppFn) do
-              throwError "e: {e}, parent: {parent}"
-            assert! (← checkChild e parent.getAppFn)
+          assert! (← checkChild e parent.getAppFn)
     else
       -- All the parents are stored in the root of the equivalence class.
       assert! (← getParents e).isEmpty
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 84e8817bef..0ffeec7e6d 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -575,6 +575,31 @@ where
     | .app f a => go f (mixHash r (hashRoot enodes a))
     | _ => mixHash r (hashRoot enodes e)
 
+/-!
+**Note**: `congrHash` and `isCongruent` must satisfy the `BEq`/`Hashable` invariant for
+`PHashSet`: if `isCongruent e₁ e₂` returns `true`, then `congrHash e₁ == congrHash e₂`.
+
+When `funCC = true`, `congrHash` hashes only the immediate function and argument:
+`mixHash (hashRoot f) (hashRoot a)`. When `funCC = false`, it recursively decomposes all
+application layers. These produce fundamentally different hash values, so `isCongruent` must
+require matching `funCC` flags. Here is the scenario that leads to a nondeterministic crash
+if mismatched flags are allowed:
+
+1. `e₁` (with `funCC = true`) is inserted into the congruence table.
+2. `e₂` (with `funCC = false`) is inserted. Its hash is computed using the non-`funCC` path.
+3. Because `hashRoot` uses pointer addresses (`ptrAddrUnsafe`), the two different hash
+   computations can accidentally collide, placing `e₂` in the same bucket as `e₁`.
+4. `isCongruent e₁ e₂` is called. If it used only `e₁`'s `funCC` flag (the old behavior),
+   the `funCC` comparison path could declare them congruent even when they have different
+   numbers of top-level arguments.
+5. `addCongrTable` calls `pushEqHEq e₂ e₁ congrPlaceholderProof`, where `e₂` is the new
+   node with `funCC = false`.
+6. During proof reconstruction, `mkCongrProof e₂ e₁` checks `useFunCC e₂ = false`, enters
+   the standard (non-`funCC`) proof path, and hits `assert! rhs.getAppNumArgs == numArgs`
+   because `e₁` and `e₂` have different argument counts.
+
+This was observed as a nondeterministic crash in Mathlib (e.g., at `Analysis/ODE/PicardLindelof.lean`).
+-/
 /-- Returns `true` if `e₁` and `e₂` are congruent modulo the equivalence classes in `enodes`. -/
 private partial def isCongruent (enodes : ENodeMap) (e₁ e₂ : Expr) : Bool :=
   if let .forallE _ d₁ b₁ _ := e₁ then
@@ -600,7 +625,14 @@ private partial def isCongruent (enodes : ENodeMap) (e₁ e₂ : Expr) : Bool :=
       **Note**: We are not in `MetaM` here. Thus, we cannot check whether `f` and `g` have the same type.
       So, we approximate and try to handle this issue when generating the proof term.
       -/
-      hasSameRoot enodes a b && hasSameRoot enodes f g
+      useFunCC' enodes e₂ && hasSameRoot enodes a b && hasSameRoot enodes f g
+    else if useFunCC' enodes e₂ then
+      /-
+      Mismatched `funCC` flags: `e₁` uses first-order congruence, `e₂` uses higher-order.
+      They hash differently (via `congrHash`), so declaring them congruent here would violate
+      the `BEq`/`Hashable` consistency invariant required by `PHashSet`.
+      -/
+      false
     else
       hasSameRoot enodes a b && go f g
 where
diff --git a/tests/elab/grind_congr_hash_issue.lean b/tests/elab/grind_congr_hash_issue.lean
index 9ef45b1024..606c9bcaa0 100644
--- a/tests/elab/grind_congr_hash_issue.lean
+++ b/tests/elab/grind_congr_hash_issue.lean
@@ -24,3 +24,9 @@ example
       a = b →
       x = y := by
   grind
+
+-- funCC congruence: `h a` and `k` are in the same equivalence class as functions,
+-- so `h a b c = k b c` should follow.
+example (h : Nat → Nat → Nat → Nat) (k : Nat → Nat → Nat)
+    : h a = k → h a b c = k b c := by
+  grind