diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean
index 9343a7ace2..e1b6ab2590 100644
--- a/src/Lean/Meta/Tactic/ElimInfo.lean
+++ b/src/Lean/Meta/Tactic/ElimInfo.lean
@@ -37,6 +37,15 @@ structure ElimInfo where
   altsInfo   : Array ElimAltInfo := #[]
   deriving Repr, Inhabited
 
+
+/-- Given the type `t` of an alternative, determines the number of parameters
+(.forall and .let)-bound, and whether the conclusion is a `motive`-application.  -/
+def altArity (motive : Expr) (n : Nat) : Expr → Nat × Bool
+  | .forallE _ _ b _ => altArity motive (n+1) b
+  | .letE _ _ _ b _ => altArity motive (n+1) b
+  | conclusion => (n, conclusion.getAppFn == motive)
+
+
 def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do
   let elimType ← inferType elimExpr
   trace[Elab.induction] "eliminator {indentExpr elimExpr}\nhas type{indentExpr elimType}"
@@ -64,8 +73,7 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
       if x != motive && !targets.contains x then
         let xDecl ← x.fvarId!.getDecl
         if xDecl.binderInfo.isExplicit then
-          let (numFields, provesMotive) ← forallTelescopeReducing xDecl.type fun args concl =>
-            pure (args.size, concl.getAppFn == motive)
+          let (numFields, provesMotive) := altArity motive 0 xDecl.type
           let name := xDecl.userName
           let declName? := do
             let base ← baseDeclName?
diff --git a/tests/lean/run/indUsingLet.lean b/tests/lean/run/indUsingLet.lean
new file mode 100644
index 0000000000..97056e9ba1
--- /dev/null
+++ b/tests/lean/run/indUsingLet.lean
@@ -0,0 +1,14 @@
+theorem some_induction
+  {motive : Nat → Prop}
+  (zero : motive 0)
+  (succ : forall n, 0 < n → let m := n - 1; motive m → motive n) :
+  ∀ n, motive n
+  | 0 => zero
+  | n+1 => succ (n+1) (Nat.zero_lt_succ n) (some_induction zero succ n)
+
+
+example (n : Nat) : n = n := by
+  induction n using some_induction
+  case zero => rfl
+  case succ n _h _m _IH =>
+    rfl