diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean
index 1cd559ab97..a1e5cbaeec 100644
--- a/src/Lean/Meta/Match/MatcherApp/Transform.lean
+++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean
@@ -22,8 +22,10 @@ private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNu
     let typeNew ← whnfD typeNew
     match typeNew with
     | Expr.forallE _ d b _ =>
-      let (alt, refined) ← forallBoundedTelescope d (some numParams) fun xs d => do
-        let alt ← try instantiateLambda alt xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
+      let (alt, refined) ← lambdaBoundedTelescope alt numParams fun xs alt => do
+        unless xs.size == numParams do
+          throwError "unexpected matcher application, alternative must have {numParams} parameters"
+        let d ← try instantiateForall d xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
         forallBoundedTelescope d (some 1) fun x _ => do
           let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative
           let refined ← if refined then
diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out
index bc6bb49864..f7a7831b35 100644
--- a/tests/lean/guessLexFailures.lean.expected.out
+++ b/tests/lean/guessLexFailures.lean.expected.out
@@ -155,5 +155,5 @@ guessLexFailures.lean:131:14-131:31: error: failed to prove termination, possibl
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
-m n✝ n : Nat
-⊢ n < n✝ + 1
+n✝ m n : Nat
+⊢ n < n✝
diff --git a/tests/lean/run/issue10976.lean b/tests/lean/run/issue10976.lean
new file mode 100644
index 0000000000..c02814f4f3
--- /dev/null
+++ b/tests/lean/run/issue10976.lean
@@ -0,0 +1,16 @@
+-- The variable names should be `a1` and `b1`
+
+/--
+error: Failed: `fail` tactic was invoked
+a1 b1 : Nat
+⊢ a1 + b1 < a1.succ + b1.succ
+-/
+#guard_msgs in
+def f (a b : Nat) := match a with
+| 0 => 0
+| a1+1 => match b with
+  | 0 => 0
+  | b1+1 => f a1 b1
+termination_by a+b
+decreasing_by
+  fail