diff --git a/RELEASES.md b/RELEASES.md
index 81934c19b3..6625d29201 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -23,9 +23,8 @@ v4.8.0 (development in progress)
 
 * New command `derive_functional_induction`:
 
-  Derived from the definition of a (possibly mutually) recursive function
-  defined by well-founded recursion, a **functional induction principle** is
-  tailored to proofs about that function. For example from:
+  Derived from the definition of a (possibly mutually) recursive function, a **functional induction
+  principle** is created that is tailored to proofs about that function. For example from:
   ```
   def ackermann : Nat → Nat → Nat
     | 0, m => m + 1
@@ -41,6 +40,11 @@ v4.8.0 (development in progress)
     (x x : Nat) : motive x x
   ```
 
+  It can be used in the `induction` tactic using the `using` syntax:
+  ```
+  induction n, m using ackermann.induct
+  ```
+
 * The termination checker now recognizes more recursion patterns without an
   explicit `termination_by`. In particular the idiom of counting up to an upper
   bound, as in
diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean
index 6715f05559..4d304e6d59 100644
--- a/src/Lean/Meta/Match/MatcherApp/Transform.lean
+++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean
@@ -291,7 +291,7 @@ def transform
     let aux1 := mkApp aux1 motive'
     let aux1 := mkAppN aux1 discrs'
     unless (← isTypeCorrect aux1) do
-      logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux1}"
+      logError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}"
       check aux1
     let origAltTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux1)
 
@@ -299,7 +299,7 @@ def transform
     let aux2 := mkApp aux2 motive'
     let aux2 := mkAppN aux2 discrs'
     unless (← isTypeCorrect aux2) do
-      logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux2}"
+      logError m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}"
       check aux2
     let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux2)
 
@@ -339,7 +339,6 @@ def transform
     let aux := mkApp aux motive'
     let aux := mkAppN aux discrs'
     unless (← isTypeCorrect aux) do
-      -- check aux
       logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux}"
       check aux
     let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux)
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 8db1be3f10..05c2de08fd 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -14,13 +14,14 @@ import Lean.Meta.Injective -- for elimOptParam
 import Lean.Meta.ArgsPacker
 import Lean.Elab.PreDefinition.WF.Eqns
 import Lean.Elab.Command
+import Lean.Meta.Tactic.ElimInfo
 
 /-!
-This module contains code to derive, from the definition of a recursive function
-(or mutually recursive functions) defined by well-founded recursion, a
-**functional induction principle** tailored to proofs about that function(s). For
-example from:
+This module contains code to derive, from the definition of a recursive function (structural or
+well-founded, possibly mutual), a **functional induction principle** tailored to proofs about that
+function(s).
 
+For example from:
 ```
 def ackermann : Nat → Nat → Nat
   | 0, m => m + 1
@@ -59,7 +60,7 @@ by `MVarId.cleanup`).
 Mutual recursion is supported and results in multiple motives.
 
 
-## Implementation overview
+## Implementation overview (well-founded recursion)
 
 For a non-mutual, unary function `foo` (or else for the `_unary` function), we
 
@@ -129,6 +130,8 @@ For a non-mutual, unary function `foo` (or else for the `_unary` function), we
 
 The resulting term then becomes `foo.induct` at its inferred type.
 
+## Implementation overview (mutual/non-unary well-founded recursion)
+
 If `foo` is not unary and/or part of a mutual reduction, then the induction theorem for `foo._unary`
 (i.e. the unary non-mutual recursion function produced by the equation compiler)
 of the form
@@ -154,8 +157,30 @@ foo.induct : {motive1 : a → b → Prop} {motive2 : c → Prop} →
   (x : a) → (y : b) → motive1 x y
 ```
 
+## Implementation overview (structural recursion)
+
+When handling structural recursion, the overall approach is the same, with the following
+differences:
+
+* Instead of `WellFounded.fix` we look for a `.brecOn` application, using `isBRecOnRecursor`
+
+  Despite its name, this function does *not* recognize the `.brecOn` of inductive *predicates*,
+  which we also do not support at this point.
+
+* The elaboration of structurally recursive function can handle extra arguments. We keep the
+  `motive` parameters in the original order.
+
+* The “induction hyothesis” in a `.brecOn` call is a `below x` term that contains all the possible
+  recursive calls, whic are projected out using `.fst.snd.…`. The `is_wf` flag that we pass down
+  tells us which form of induction hypothesis we are looking for.
+
+* If we have nested recursion (`foo n (foo m acc))`), then we need to infer the argument `m` of the
+  nested call `ih.fst.snd acc`. To do so reliably, we replace the `ih` with the “new `ih`”, which
+  will have type `motive m acc`, and since `motive` is a FVar we can then read off the arguments
+  off this nicely..
 -/
 
+
 set_option autoImplicit false
 
 namespace Lean.Tactic.FunInd
@@ -172,26 +197,75 @@ def removeLamda {n} [MonadLiftT MetaM n] [MonadError n] [MonadNameGenerator n] [
   let b := b.instantiate1 (.fvar x)
   k x b
 
-/-- Replace calls to oldIH back to calls to the original function. At the end, if `oldIH` occurs, an error is thrown. -/
-partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do
+/-- Structural recursion only: recognizes `oldIH.fst.snd a₁ a₂` and returns `newIH.fst.snd`. -/
+partial def isPProdProj (oldIH newIH : FVarId) (e : Expr) : MetaM (Option Expr) := do
+  if e.isAppOfArity ``PProd.fst 3 then
+    if let some e' ← isPProdProj oldIH newIH e.appArg! then
+      return some (← mkAppM ``PProd.fst #[e'])
+    else
+      return none
+  else if e.isAppOfArity ``PProd.snd 3 then
+    if let some e' ← isPProdProj oldIH newIH e.appArg! then
+      return some (← mkAppM ``PProd.snd #[e'])
+    else
+      return none
+  else if e.isFVarOf oldIH then
+    return some (mkFVar newIH)
+  else
+    return none
+
+/--
+Structural recursion only:
+Recognizes `oldIH.fst.snd a₁ a₂` and returns `newIH.fst.snd` and `#[a₁, a₂]`.
+-/
+def isPProdProjWithArgs (oldIH newIH : FVarId) (e : Expr) : MetaM (Option (Expr × Array Expr)) := do
+  if e.isAppOf ``PProd.fst || e.isAppOf ``PProd.snd then
+    let arity := e.getAppNumArgs
+    unless 3 ≤ arity do return none
+    let args := e.getAppArgsN (arity - 3)
+    if let some e' ← isPProdProj oldIH newIH (e.stripArgsN (arity - 3)) then
+      return some (e', args)
+  return none
+
+/--
+Replace calls to oldIH back to calls to the original function. At the end, if `oldIH` occurs, an
+error is thrown.
+
+The `newIH` will not show up in the output of `foldCalls`, we use it as a helper to infer the
+argument of nested recursive calls when we have structural recursion.
+-/
+partial def foldCalls (is_wf : Bool) (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM Expr := do
   unless e.containsFVar oldIH do
     return e
 
-  if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
-    let #[arg, _proof] := e.getAppArgs | unreachable!
-    let arg' ← foldCalls fn oldIH arg
-    return .app fn arg'
+  if is_wf then
+    if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
+      let #[arg, _proof] := e.getAppArgs | unreachable!
+      let arg' ← foldCalls is_wf fn oldIH newIH arg
+      return .app fn arg'
+  else
+    if let some (e', args) ← isPProdProjWithArgs oldIH newIH e then
+      let t ← whnf (← inferType e')
+      let e' ← forallTelescopeReducing t fun xs t' => do
+        unless t'.getAppFn.isFVar do -- we expect an application of the `motive` FVar here
+          throwError m!"Unexpected type {t} of {e}: Reduced to application of {t'.getAppFn}"
+        mkLambdaFVars xs (fn.beta t'.getAppArgs)
+      let args' ← args.mapM (foldCalls is_wf fn oldIH newIH)
+      let e' := e'.beta args'
+      unless ← isTypeCorrect e' do
+        throwError m!"foldCalls: type incorrect after replacing recursive call:{indentExpr e'}"
+      return e'
 
   if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
       let matcherApp' ← matcherApp.transform
-        (onParams := foldCalls fn oldIH)
+        (onParams := foldCalls is_wf fn oldIH newIH)
         (onMotive := fun _motiveArgs motiveBody => do
           let some (_extra, body) := motiveBody.arrow? | throwError "motive not an arrow"
-          foldCalls fn oldIH body)
+          foldCalls is_wf fn oldIH newIH body)
         (onAlt := fun _altType alt => do
           removeLamda alt fun oldIH alt => do
-            foldCalls fn oldIH alt)
+            foldCalls is_wf fn oldIH newIH alt)
         (onRemaining := fun _ => pure #[])
       return matcherApp'.toExpr
 
@@ -203,43 +277,43 @@ partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do
     let e' ← withTransparency .all do whnf e
     if e == e' then
       throwError "foldCalls: cannot reduce application of {e.getAppFn} in {indentExpr e} "
-    return ← foldCalls fn oldIH e'
+    return ← foldCalls is_wf fn oldIH newIH e'
 
   if let some (n, t, v, b) := e.letFun? then
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLocalDecl n .default t' fun x => do
-      let b' ← foldCalls fn oldIH (b.instantiate1 x)
+      let b' ← foldCalls is_wf fn oldIH newIH (b.instantiate1 x)
       mkLetFun x v' b'
 
   match e with
   | .app e1 e2 =>
-    return .app (← foldCalls fn oldIH e1) (← foldCalls fn oldIH e2)
+    return .app (← foldCalls is_wf fn oldIH newIH e1) (← foldCalls is_wf fn oldIH newIH e2)
 
   | .lam n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let body' ← foldCalls fn oldIH (body.instantiate1 x)
+      let body' ← foldCalls is_wf fn oldIH newIH (body.instantiate1 x)
       mkLambdaFVars #[x] body'
 
   | .forallE n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let body' ← foldCalls fn oldIH (body.instantiate1 x)
+      let body' ← foldCalls is_wf fn oldIH newIH (body.instantiate1 x)
       mkForallFVars #[x] body'
 
   | .letE n t v b _ =>
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t' v' fun x => do
-      let b' ← foldCalls fn oldIH (b.instantiate1 x)
+      let b' ← foldCalls is_wf fn oldIH newIH (b.instantiate1 x)
       mkLetFVars  #[x] b'
 
   | .mdata m b =>
-    return .mdata m (← foldCalls fn oldIH b)
+    return .mdata m (← foldCalls is_wf fn oldIH newIH b)
 
   | .proj t i e =>
-    return .proj t i (← foldCalls fn oldIH e)
+    return .proj t i (← foldCalls is_wf fn oldIH newIH e)
 
   | .sort .. | .lit .. | .const .. | .mvar .. | .bvar .. =>
     unreachable! -- cannot contain free variables, so early exit above kicks in
@@ -248,35 +322,56 @@ partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do
     throwError m!"collectIHs: cannot eliminate unsaturated call to induction hypothesis"
 
 
--- Non-tail-positions: Collect induction hypotheses
--- (TODO: Worth folding with `foldCalls`, like before?)
--- (TODO: Accumulated with a left fold)
-partial def collectIHs (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Array Expr) := do
+/-
+In non-tail-positions, we collect the induction hypotheses from all the recursive calls.
+-/
+-- We could run `collectIHs` and `foldCalls` together, and save a few traversals. Not sure if it
+-- worth the extra code complexity.
+-- Also, this way of collecting arrays is not as efficient as a left-fold, but we do not expect
+-- large arrays here.
+partial def collectIHs (is_wf : Bool) (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Array Expr) := do
   unless e.containsFVar oldIH do
     return #[]
 
-  if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
-    let #[arg, proof] := e.getAppArgs  | unreachable!
+  if is_wf then
+    if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
+      let #[arg, proof] := e.getAppArgs  | unreachable!
 
-    let arg' ← foldCalls fn oldIH arg
-    let proof' ← foldCalls fn oldIH proof
-    let ihs ← collectIHs fn oldIH newIH arg
+      let arg' ← foldCalls is_wf fn oldIH newIH arg
+      let proof' ← foldCalls is_wf fn oldIH newIH proof
+      let ihs ← collectIHs is_wf fn oldIH newIH arg
+
+      return ihs.push (mkApp2 (.fvar newIH) arg' proof')
+  else
+    if let some (e', args) ← isPProdProjWithArgs oldIH newIH e then
+      let args' ← args.mapM (foldCalls is_wf fn oldIH newIH)
+      let ihs ← args.concatMapM (collectIHs is_wf fn oldIH newIH)
+      let t ← whnf (← inferType e')
+      let arity ← forallTelescopeReducing t fun xs t' => do
+        unless t'.getAppFn.isFVar do -- we expect an application of the `motive` FVar here
+          throwError m!"Unexpected type {t} of {e}: Reduced to application of {t'.getAppFn}"
+        pure xs.size
+      let e' := mkAppN e' args'[:arity]
+      let eTyp ← inferType e'
+      -- The inferred type that comes out of motive projections has beta redexes
+      let eType' := eTyp.headBeta
+      return ihs.push (← mkExpectedTypeHint e' eType')
 
-    return ihs.push (mkApp2 (.fvar newIH) arg' proof')
 
   if let some (n, t, v, b) := e.letFun? then
-    let ihs1 ← collectIHs fn oldIH newIH v
-    let v' ← foldCalls fn oldIH v
+    let ihs1 ← collectIHs is_wf fn oldIH newIH v
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t v' fun x => do
-      let ihs2 ← collectIHs fn oldIH newIH (b.instantiate1 x)
+      let ihs2 ← collectIHs is_wf fn oldIH newIH (b.instantiate1 x)
       let ihs2 ← ihs2.mapM (mkLetFVars (usedLetOnly := true) #[x] ·)
       return ihs1 ++ ihs2
 
+
   if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
 
       let matcherApp' ← matcherApp.transform
-        (onParams := foldCalls fn oldIH)
+        (onParams := foldCalls is_wf fn oldIH newIH)
         (onMotive := fun xs _body => do
           -- Remove the old IH that was added in mkFix
           let eType ← newIH.getType
@@ -294,7 +389,7 @@ partial def collectIHs (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Ar
           removeLamda alt fun oldIH' alt => do
             forallBoundedTelescope altType (some 1) fun newIH' _goal' => do
               let #[newIH'] := newIH' | unreachable!
-              let altIHs ← collectIHs fn oldIH' newIH'.fvarId! alt
+              let altIHs ← collectIHs is_wf fn oldIH' newIH'.fvarId! alt
               let altIH ← mkAndIntroN altIHs
               mkLambdaFVars #[newIH'] altIH)
         (onRemaining := fun _ => pure #[mkFVar newIH])
@@ -310,40 +405,40 @@ partial def collectIHs (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Ar
     let e' ← withTransparency .all do whnf e
     if e == e' then
       throwError "collectIHs: cannot reduce application of {e.getAppFn} in {indentExpr e} "
-    return ← collectIHs fn oldIH newIH e'
+    return ← collectIHs is_wf fn oldIH newIH e'
 
   if e.getAppArgs.any (·.isFVarOf oldIH) then
     throwError "collectIHs: could not collect recursive calls from call {indentExpr e}"
 
   match e with
   | .letE n t v b _ =>
-    let ihs1 ← collectIHs fn oldIH newIH v
-    let v' ← foldCalls fn oldIH v
+    let ihs1 ← collectIHs is_wf fn oldIH newIH v
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t v' fun x => do
-      let ihs2 ← collectIHs fn oldIH newIH (b.instantiate1 x)
+      let ihs2 ← collectIHs is_wf fn oldIH newIH (b.instantiate1 x)
       let ihs2 ← ihs2.mapM (mkLetFVars (usedLetOnly := true) #[x] ·)
       return ihs1 ++ ihs2
 
   | .app e1 e2 =>
-    return (← collectIHs fn oldIH newIH e1) ++ (← collectIHs fn oldIH newIH e2)
+    return (← collectIHs is_wf fn oldIH newIH e1) ++ (← collectIHs is_wf fn oldIH newIH e2)
 
   | .proj _ _ e =>
-    return ← collectIHs fn oldIH newIH e
+    return ← collectIHs is_wf fn oldIH newIH e
 
   | .forallE n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let ihs ← collectIHs fn oldIH newIH (body.instantiate1 x)
+      let ihs ← collectIHs is_wf fn oldIH newIH (body.instantiate1 x)
       ihs.mapM (mkLambdaFVars (usedOnly := true) #[x])
 
   | .lam n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let ihs ← collectIHs fn oldIH newIH (body.instantiate1 x)
+      let ihs ← collectIHs is_wf fn oldIH newIH (body.instantiate1 x)
       ihs.mapM (mkLambdaFVars (usedOnly := true) #[x])
 
   | .mdata _m b =>
-    return ← collectIHs fn oldIH newIH b
+    return ← collectIHs is_wf fn oldIH newIH b
 
   | .sort .. | .lit .. | .const .. | .mvar .. | .bvar .. =>
     unreachable! -- cannot contain free variables, so early exit above kicks in
@@ -393,9 +488,9 @@ abbrev M α := StateT (Array MVarId) MetaM α
 
 
 /-- Base case of `buildInductionBody`: Construct a case for the final induction hypthesis.  -/
-def buildInductionCase (fn : Expr) (oldIH newIH : FVarId) (toClear toPreserve : Array FVarId)
+def buildInductionCase (is_wf : Bool) (fn : Expr) (oldIH newIH : FVarId) (toClear toPreserve : Array FVarId)
     (goal : Expr) (IHs : Array Expr) (e : Expr) : M Expr := do
-  let IHs := IHs ++ (← collectIHs fn oldIH newIH e)
+  let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH e)
   let IHs ← deduplicateIHs IHs
 
   let mvar ← mkFreshExprSyntheticOpaqueMVar goal (tag := `hyp)
@@ -448,30 +543,45 @@ Builds an expression of type `goal` by replicating the expression `e` into its t
 where it calls `buildInductionCase`. Collects the cases of the final induction hypothesis
 as `MVars` as it goes.
 -/
-partial def buildInductionBody (fn : Expr) (toClear toPreserve : Array FVarId)
+partial def buildInductionBody (is_wf : Bool) (fn : Expr) (toClear toPreserve : Array FVarId)
     (goal : Expr) (oldIH newIH : FVarId) (IHs : Array Expr) (e : Expr) : M Expr := do
   -- logInfo m!"buildInductionBody {e}"
 
-  if e.isDIte then
-    let #[_α, c, h, t, f] := e.getAppArgs | unreachable!
-    let IHs := IHs ++ (← collectIHs fn oldIH newIH c)
-    let c' ← foldCalls fn oldIH c
-    let h' ← foldCalls fn oldIH h
+  -- if-then-else cause case split:
+  match_expr e with
+  | ite _α c h t f =>
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH c)
+    let c' ← foldCalls is_wf fn oldIH newIH c
+    let h' ← foldCalls is_wf fn oldIH newIH h
     let t' ← withLocalDecl `h .default c' fun h => do
-      let t ← instantiateLambda t #[h]
-      let t' ← buildInductionBody fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs t
+      let t' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs t
       mkLambdaFVars #[h] t'
     let f' ← withLocalDecl `h .default (mkNot c') fun h => do
-      let f ← instantiateLambda f #[h]
-      let f' ← buildInductionBody fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs f
+      let f' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs f
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
+  | dite _α c h t f =>
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH c)
+    let c' ← foldCalls is_wf fn oldIH newIH c
+    let h' ← foldCalls is_wf fn oldIH newIH h
+    let t' ← withLocalDecl `h .default c' fun h => do
+      let t ← instantiateLambda t #[h]
+      let t' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs t
+      mkLambdaFVars #[h] t'
+    let f' ← withLocalDecl `h .default (mkNot c') fun h => do
+      let f ← instantiateLambda f #[h]
+      let f' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs f
+      mkLambdaFVars #[h] f'
+    let u ← getLevel goal
+    return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
+  | _ =>
 
+  -- match and casesOn application cause case splitting
   if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
     -- Collect IHs from the parameters and discrs of the matcher
     let paramsAndDiscrs := matcherApp.params ++ matcherApp.discrs
-    let IHs := IHs ++ (← paramsAndDiscrs.concatMapM (collectIHs fn oldIH newIH ·))
+    let IHs := IHs ++ (← paramsAndDiscrs.concatMapM (collectIHs is_wf fn oldIH newIH ·))
 
     -- Calculate motive
     let eType ← newIH.getType
@@ -483,13 +593,13 @@ partial def buildInductionBody (fn : Expr) (toClear toPreserve : Array FVarId)
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
       let matcherApp' ← matcherApp.transform (useSplitter := true)
         (addEqualities := mask.map not)
-        (onParams := (foldCalls fn oldIH ·))
+        (onParams := (foldCalls is_wf fn oldIH newIH ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => do
           removeLamda alt fun oldIH' alt => do
             forallBoundedTelescope expAltType (some 1) fun newIH' goal' => do
               let #[newIH'] := newIH' | unreachable!
-              let alt' ← buildInductionBody fn (toClear.push newIH'.fvarId!) toPreserve goal' oldIH' newIH'.fvarId! IHs alt
+              let alt' ← buildInductionBody is_wf fn (toClear.push newIH'.fvarId!) toPreserve goal' oldIH' newIH'.fvarId! IHs alt
               mkLambdaFVars #[newIH'] alt')
         (onRemaining := fun _ => pure #[.fvar newIH])
       return matcherApp'.toExpr
@@ -502,29 +612,29 @@ partial def buildInductionBody (fn : Expr) (toClear toPreserve : Array FVarId)
 
       let matcherApp' ← matcherApp.transform (useSplitter := true)
         (addEqualities := mask.map not)
-        (onParams := (foldCalls fn oldIH ·))
+        (onParams := (foldCalls is_wf fn oldIH newIH ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => do
-          buildInductionBody fn toClear toPreserve expAltType oldIH newIH IHs alt)
+          buildInductionBody is_wf fn toClear toPreserve expAltType oldIH newIH IHs alt)
       return matcherApp'.toExpr
 
   if let .letE n t v b _ := e then
-    let IHs := IHs ++ (← collectIHs fn oldIH newIH v)
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH v)
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t' v' fun x => do
-      let b' ← buildInductionBody fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
+      let b' ← buildInductionBody is_wf fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
       mkLetFVars #[x] b'
 
   if let some (n, t, v, b) := e.letFun? then
-    let IHs := IHs ++ (← collectIHs fn oldIH newIH v)
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH v)
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLocalDecl n .default t' fun x => do
-      let b' ← buildInductionBody fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
+      let b' ← buildInductionBody is_wf fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
       mkLetFun x v' b'
 
-  buildInductionCase fn oldIH newIH toClear toPreserve goal IHs e
+  liftM <| buildInductionCase is_wf fn oldIH newIH toClear toPreserve goal IHs e
 
 /--
 Given an expression `e` with metavariables
@@ -555,17 +665,86 @@ def abstractIndependentMVars (mvars : Array MVarId) (x : FVarId) (e : Expr) : Me
         mvar.assign x
       mkLambdaFVars xs (← instantiateMVars e)
 
-partial def findFixF {α} (name : Name) (e : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α := do
-  lambdaTelescope e fun params body => do
-    if body.isAppOf ``WellFounded.fixF then
-      k params body
-    else if body.isAppOf ``WellFounded.fix then
-      findFixF name (← unfoldDefinition body) fun args e' => k (params ++ args) e'
-    else
-      throwError m!"Function {name} does not look like a function defined by well-founded " ++
-        m!"recursion.\nNB: If {name} is not itself recursive, but contains an inner recursive " ++
-        m!"function (via `let rec` or `where`), try `{name}.go` where `go` is name of the inner " ++
-        "function."
+/--
+This function looks that the body of a recursive function and looks for either users of
+`fix`, `fixF` or a `.brecOn`, and abstracts over the differences between them. It passes
+to the continuation
+
+* whether we are using well-founded recursion
+* the fixed parameters of the function body
+* the varying parameters of the function body (this includes both the targets of the
+  recursion and extra parameters passed to the recursor)
+* the position of the motive/induction hypothesis in the body's arguments
+* the body, as passed to the recursor. Expected to be a lambda that takes the
+  varying paramters and the motive
+* a function to re-assemble the call with a new Motive. The resulting expression expects
+  the new body next, so that the expected type of the body can be inferred
+* a function to finish assembling the call with the new body.
+-/
+def findRecursor {α} (name : Name) (varNames : Array Name) (e : Expr)
+    (k :(is_wf : Bool) →
+        (fixedParams : Array Expr) →
+        (varyingParams : Array Expr) →
+        (motivePosInBody : Nat) →
+        (body : Expr) →
+        (mkAppMotive : Expr → MetaM Expr) →
+        (mkAppBody : Expr → Expr → Expr) →
+        MetaM α) :
+    MetaM α := do
+  -- Uses of WellFounded.fix can be partially applied. Here we eta-expand the body
+  -- to avoid dealing with this
+  let e ← lambdaTelescope e fun params body => do mkLambdaFVars params (← etaExpand body)
+  lambdaTelescope e fun params body => body.withApp fun f args => do
+    MatcherApp.withUserNames params varNames do
+      if not f.isConst then err else
+      if isBRecOnRecursor (← getEnv) f.constName! then
+        let elimInfo ← getElimExprInfo f
+        let targets : Array Expr := elimInfo.targetsPos.map (args[·]!)
+        let body := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size]!
+        let extraArgs : Array Expr := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size + 1:]
+
+        let fixedParams := params.filter fun x => !(targets.contains x || extraArgs.contains x)
+        let varyingParams := params.filter fun x => targets.contains x || extraArgs.contains x
+        unless params == fixedParams ++ varyingParams do
+          throwError "functional induction: unexpected order of fixed and varying parameters:{indentExpr e}"
+        -- we assume the motive's universe parameter is the first
+        unless 1 ≤ f.constLevels!.length do
+          throwError "functional induction: unexpected recursor: {f} has no universe parameters"
+        let us := f.constLevels!.set 0 levelZero
+
+        let value := mkAppN (.const f.constName us) (args[:elimInfo.motivePos])
+        k false fixedParams varyingParams targets.size body
+          (fun newMotive => do
+            -- We may have to reorder the parameters for motive before passing it to brec
+            let brecMotive ← mkLambdaFVars targets
+              (← mkForallFVars extraArgs (mkAppN newMotive varyingParams))
+            return mkAppN (mkApp value brecMotive) targets)
+          (fun value newBody => mkAppN (.app value newBody) extraArgs)
+      else if Name.isSuffixOf `brecOn f.constName! then
+        throwError m!"Function {name} is defined in a way not supported by functional induction, " ++
+          "for example by recursion over an inductive predicate."
+      else match_expr body with
+      | WellFounded.fixF α rel _motive body target acc =>
+        unless params.back == target do
+          throwError "functional induction: expected the target as last parameter{indentExpr e}"
+        let value := .const ``WellFounded.fixF [f.constLevels![0]!, levelZero]
+        k true params.pop #[params.back] 1 body
+          (fun newMotive => pure (mkApp3 value α rel newMotive))
+          (fun value newBody => mkApp2 value newBody acc)
+      | WellFounded.fix α _motive rel wf body target =>
+        unless params.back == target do
+          throwError "functional induction: expected the target as last parameter{indentExpr e}"
+        let value := .const ``WellFounded.fix [f.constLevels![0]!, levelZero]
+        k true params.pop #[target] 1 body
+          (fun newMotive => pure (mkApp4 value α newMotive rel wf))
+          (fun value newBody => mkApp2 value newBody target)
+      | _ => err
+  where
+    err := throwError m!"Function {name} does not look like a function defined by recursion." ++
+      m!"\nNB: If {name} is not itself recursive, but contains an inner recursive " ++
+      m!"function (via `let rec` or `where`), try `{name}.go` where `go` is name of the inner " ++
+      "function."
+
 
 /--
 Given a definition `foo` defined via `WellFounded.fixF`, derive a suitable induction principle
@@ -576,62 +755,60 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
   if ← hasConst inductName then return inductName
 
   let info ← getConstInfoDefn name
-  findFixF name info.value fun params body => body.withApp fun f fixArgs => do
-    -- logInfo f!"{fixArgs}"
-    unless params.size > 0 do
-      throwError "Value of {name} is not a lambda application"
-    unless f.isConstOf ``WellFounded.fixF do
-      throwError "Term isn’t application of {``WellFounded.fixF}, but of {f}"
-    let #[argType, rel, _motive, body, arg, acc] := fixArgs |
-      throwError "Application of WellFounded.fixF has wrong arity {fixArgs.size}"
-    unless ← isDefEq arg params.back do
-      throwError "fixF application argument {arg} is not function argument "
-    let [argLevel, _motiveLevel] := f.constLevels! | unreachable!
 
-    let motiveType ← mkArrow argType (.sort levelZero)
-    withLocalDecl `motive .default motiveType fun motive => do
+  let varNames ← forallTelescope info.type fun xs _ => xs.mapM (·.fvarId!.getUserName)
 
-    let e' := mkApp3 (.const ``WellFounded.fixF [argLevel, levelZero]) argType rel motive
-    let fn := mkAppN (.const name (info.levelParams.map mkLevelParam)) params.pop
-    let (body', mvars) ← StateT.run (s := {}) <| forallTelescope (← inferType e').bindingDomain! fun xs _ => do
-      let #[param, genIH] := xs | unreachable!
-      -- open body with the same arg
-      let body ← instantiateLambda body #[param]
-      removeLamda body fun oldIH body => do
-        let body' ← buildInductionBody fn #[genIH.fvarId!] #[] (.app motive param) oldIH genIH.fvarId! #[] body
-        if body'.containsFVar oldIH then
-          throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
-        mkLambdaFVars #[param, genIH] body'
-
-    let e' := mkApp3 e' body' arg acc
-
-    let e' ← mkLambdaFVars #[params.back] e'
-    let e' ← abstractIndependentMVars mvars motive.fvarId! e'
-    let e' ← mkLambdaFVars #[motive] e'
-
-    -- We could pass (usedOnly := true) below, and get nicer induction principles that
-    -- do do not mention odd unused parameters.
-    -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
-    -- that derives them from an function application in the goal) is harder, as
-    -- one would have to infer or keep track of which parameters to pass.
-    -- So for now lets just keep them around.
-    let e' ← mkLambdaFVars (binderInfoForMVars := .default) params.pop e'
-    let e' ← instantiateMVars e'
-
-    let eTyp ← inferType e'
-    let eTyp ← elimOptParam eTyp
-    -- logInfo m!"eTyp: {eTyp}"
-    unless (← isTypeCorrect e') do
-      logError m!"failed to derive induction priciple:{indentExpr e'}"
+  let e' ← findRecursor name varNames info.value
+    fun is_wf fixedParams varyingParams motivePosInBody body mkAppMotive mkAppBody => do
+      let motiveType ← mkForallFVars varyingParams (.sort levelZero)
+      withLocalDecl `motive .default motiveType fun motive => do
+      let fn := mkAppN (.const name (info.levelParams.map mkLevelParam)) fixedParams
+      let e' ← mkAppMotive motive
       check e'
+      let (body', mvars) ← StateT.run (s := {}) do
+        forallTelescope (← inferType e').bindingDomain! fun xs goal => do
+          let arity := varyingParams.size + 1
+          if xs.size ≠ arity then
+            throwError "expected recursor argument to take {arity} parameters, got {xs}" else
+          let targets : Array Expr := xs[:motivePosInBody]
+          let genIH := xs[motivePosInBody]!
+          let extraParams := xs[motivePosInBody+1:]
+          -- open body with the same arg
+          let body ← instantiateLambda body targets
+          removeLamda body fun oldIH body => do
+            let body ← instantiateLambda body extraParams
+            let body' ← buildInductionBody is_wf fn #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! #[] body
+            if body'.containsFVar oldIH then
+              throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
+            mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
+      let e' := mkAppBody e' body'
+      let e' ← mkLambdaFVars varyingParams e'
+      let e' ← abstractIndependentMVars mvars motive.fvarId! e'
+      let e' ← mkLambdaFVars #[motive] e'
 
-    let params := (collectLevelParams {} eTyp).params
-    -- Prune unused level parameters, preserving the original order
-    let us := info.levelParams.filter (params.contains ·)
+      -- We could pass (usedOnly := true) below, and get nicer induction principles that
+      -- do do not mention odd unused parameters.
+      -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
+      -- that derives them from an function application in the goal) is harder, as
+      -- one would have to infer or keep track of which parameters to pass.
+      -- So for now lets just keep them around.
+      let e' ← mkLambdaFVars (binderInfoForMVars := .default) fixedParams e'
+      instantiateMVars e'
 
-    addDecl <| Declaration.thmDecl
-      { name := inductName, levelParams := us, type := eTyp, value := e' }
-    return inductName
+  unless (← isTypeCorrect e') do
+    logError m!"failed to derive induction priciple:{indentExpr e'}"
+    check e'
+
+  let eTyp ← inferType e'
+  let eTyp ← elimOptParam eTyp
+  -- logInfo m!"eTyp: {eTyp}"
+  let params := (collectLevelParams {} eTyp).params
+  -- Prune unused level parameters, preserving the original order
+  let us := info.levelParams.filter (params.contains ·)
+
+  addDecl <| Declaration.thmDecl
+    { name := inductName, levelParams := us, type := eTyp, value := e' }
+  return inductName
 
 /--
 In the type of `value`, reduces
diff --git a/tests/lean/run/funind_demo.lean b/tests/lean/run/funind_demo.lean
index acaa5621e5..bfae65dc85 100644
--- a/tests/lean/run/funind_demo.lean
+++ b/tests/lean/run/funind_demo.lean
@@ -27,7 +27,7 @@ derive_functional_induction Tree.rev
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
-  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (x : Tree) : motive x
+  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a
 -/
 #guard_msgs in
 #check Tree.rev.induct
diff --git a/tests/lean/run/funind_expr.lean b/tests/lean/run/funind_expr.lean
index 0161fef629..3d6177baf5 100644
--- a/tests/lean/run/funind_expr.lean
+++ b/tests/lean/run/funind_expr.lean
@@ -70,7 +70,7 @@ info: Expr.typeCheck.induct (motive : Expr → Prop) (case1 : ∀ (a : Nat), mot
       (∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
           a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False) →
         motive a → motive b → motive (a.and b))
-  (x : Expr) : motive x
+  (e : Expr) : motive e
 -/
 #guard_msgs in
 #check Expr.typeCheck.induct
diff --git a/tests/lean/run/funind_fewer_levels.lean b/tests/lean/run/funind_fewer_levels.lean
index 111ee45f4a..79a5c9b300 100644
--- a/tests/lean/run/funind_fewer_levels.lean
+++ b/tests/lean/run/funind_fewer_levels.lean
@@ -4,6 +4,26 @@ This test checks if the functional induction principle has fewer universe parame
 if the original function has a parameter that disappears.
 -/
 
+namespace Structural
+def foo.{u} : Nat → PUnit.{u}
+| 0 => .unit
+| n+1 => foo n
+
+derive_functional_induction foo
+/--
+info: Structural.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
+-/
+#guard_msgs in
+#check foo.induct
+
+example : foo n = .unit := by
+  induction n using foo.induct with
+  | case1 => unfold foo; rfl
+  | case2 n ih => unfold foo; exact ih
+
+end Structural
+
 namespace WellFounded
 def foo.{u,v} {α : Type v} : List α  → PUnit.{u}
 | [] => .unit
@@ -13,7 +33,7 @@ termination_by xs => xs
 derive_functional_induction foo
 /--
 info: WellFounded.foo.induct.{v} {α : Type v} (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) (x : List α) : motive x
+  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) : ∀ (a : List α), motive a
 -/
 #guard_msgs in
 #check foo.induct
diff --git a/tests/lean/run/funind_structural.lean b/tests/lean/run/funind_structural.lean
new file mode 100644
index 0000000000..d91cec333b
--- /dev/null
+++ b/tests/lean/run/funind_structural.lean
@@ -0,0 +1,230 @@
+import Lean.Elab.Command
+
+/-!
+This module tests functional induction principles on *structurally* recursive functions.
+-/
+
+def fib : Nat → Nat
+  | 0 | 1 => 0
+  | n+2 => fib n + fib (n+1)
+
+derive_functional_induction fib
+/--
+info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a : Nat), motive a
+-/
+#guard_msgs in
+#check fib.induct
+
+
+def binary : Nat → Nat → Nat
+  | 0, acc | 1, acc => 1 + acc
+  | n+2, acc => binary n (binary (n+1) acc)
+
+derive_functional_induction binary
+/--
+info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc)
+  (case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc) :
+  ∀ (a a_1 : Nat), motive a a_1
+-/
+#guard_msgs in
+#check binary.induct
+
+
+-- Different parameter order
+def binary' : Bool → Nat → Bool
+  | acc, 0 | acc , 1 => not acc
+  | acc, n+2 => binary' (binary' acc (n+1)) n
+
+derive_functional_induction binary'
+/--
+info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0)
+  (case2 : ∀ (acc : Bool), motive acc 1)
+  (case3 : ∀ (acc : Bool) (n : Nat), motive acc (n + 1) → motive (binary' acc (n + 1)) n → motive acc n.succ.succ) :
+  ∀ (a : Bool) (a_1 : Nat), motive a a_1
+-/
+#guard_msgs in
+#check binary'.induct
+
+def zip {α β} : List α → List β → List (α × β)
+  | [], _ => []
+  | _, [] => []
+  | x::xs, y::ys => (x, y) :: zip xs ys
+
+derive_functional_induction zip
+/--
+info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
+  (case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (x : List α), (x = [] → False) → motive x [])
+  (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) :
+  ∀ (a : List α) (a_1 : List β), motive a a_1
+-/
+#guard_msgs in
+#check zip.induct
+
+/-- Lets try ot use it! -/
+theorem zip_length {α β} (xs : List α) (ys : List β) :
+    (zip xs ys).length = xs.length.min ys.length := by
+  induction xs, ys using zip.induct
+  case case1 => simp [zip]
+  case case2 => simp [zip]
+  case case3 =>
+    simp [zip, *]
+    simp [Nat.min_def]
+    split<;>split<;> omega
+
+theorem zip_get?  {α β} (as : List α) (bs : List β) :
+    (List.zip as bs).get? i = match as.get? i, bs.get? i with
+      | some a, some b => some (a, b) | _, _ => none := by
+  induction as, bs using zip.induct generalizing i
+    <;> cases i <;> simp_all
+
+-- Testing recursion on an indexed data type
+inductive Finn : Nat → Type where
+  | fzero : {n : Nat} → Finn n
+  | fsucc : {n : Nat} → Finn n → Finn (n+1)
+
+def Finn.min (x : Bool) {n : Nat} (m : Nat) : Finn n → (f : Finn n) → Finn n
+  | fzero, _ => fzero
+  | _, fzero => fzero
+  | fsucc i, fsucc j => fsucc (Finn.min (not x) (m + 1) i j)
+
+derive_functional_induction Finn.min
+/--
+info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n → Prop)
+  (case1 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), motive x m Finn.fzero x_1)
+  (case2 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), (x_1 = Finn.fzero → False) → motive x m x_1 Finn.fzero)
+  (case3 : ∀ (x : Bool) (m n : Nat) (i j : Finn n), motive (!x) (m + 1) i j → motive x m i.fsucc j.fsucc) (x : Bool)
+  {n : Nat} (m : Nat) : ∀ (a f : Finn n), motive x m a f
+-/
+#guard_msgs in
+#check Finn.min.induct
+
+
+inductive Even : Nat → Prop where
+| zero : Even 0
+| plus2 : Even n → Even (n + 2)
+
+def idEven : Even n → Even n
+| .zero => .zero
+| .plus2 p => .plus2 (idEven p)
+/--
+error: Function idEven is defined in a way not supported by functional induction, for example by recursion over an inductive predicate.
+-/
+#guard_msgs in
+derive_functional_induction idEven
+
+
+-- Acc.brecOn is not recognized by isBRecOnRecursor:
+-- run_meta Lean.logInfo m!"{Lean.isBRecOnRecursor (← Lean.getEnv) ``Acc.brecOn}"
+def idAcc : Acc p x → Acc p x
+  | Acc.intro x f => Acc.intro x (fun y h => idAcc (f y h))
+/--
+error: Function idAcc is defined in a way not supported by functional induction, for example by recursion over an inductive predicate.
+-/
+#guard_msgs in
+derive_functional_induction idAcc
+
+namespace TreeExample
+
+inductive Tree (β : Type v) where
+  | leaf
+  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
+
+def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
+  match t with
+  | leaf => node leaf k v leaf
+  | node left key value right =>
+    if k < key then
+      node (left.insert k v) key value right
+    else if key < k then
+      node left key value (right.insert k v)
+    else
+      node left k v right
+
+derive_functional_induction Tree.insert
+
+/--
+info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (motive : Tree β → Nat → β → Prop)
+  (case1 : ∀ (k : Nat) (v : β), motive Tree.leaf k v)
+  (case2 :
+    ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β),
+      k < key → motive left k v → motive (left.node key value right) k v)
+  (case3 :
+    ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β),
+      ¬k < key → key < k → motive right k v → motive (left.node key value right) k v)
+  (case4 :
+    ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β),
+      ¬k < key → ¬key < k → motive (left.node key value right) k v)
+  (t : Tree β) (k : Nat) (v : β) : motive t k v
+-/
+#guard_msgs in
+#check Tree.insert.induct
+
+end TreeExample
+
+namespace Term
+
+inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
+  | nil  : HList β []
+  | cons : β i → HList β is → HList β (i::is)
+
+inductive Member : α → List α → Type
+  | head : Member a (a::as)
+  | tail : Member a bs → Member a (b::bs)
+
+def HList.get : HList β is → Member i is → β i
+  | .cons a as, .head => a
+  | .cons _ as, .tail h => as.get h
+
+inductive Ty where
+  | nat
+  | fn : Ty → Ty → Ty
+
+@[reducible] def Ty.denote : Ty → Type
+  | nat    => Nat
+  | fn a b => a.denote → b.denote
+
+inductive Term : List Ty → Ty → Type
+  | var   : Member ty ctx → Term ctx ty
+  | const : Nat → Term ctx .nat
+  | plus  : Term ctx .nat → Term ctx .nat → Term ctx .nat
+  | app   : Term ctx (.fn dom ran) → Term ctx dom → Term ctx ran
+  | lam   : Term (.cons dom ctx) ran → Term ctx (.fn dom ran)
+  | let   : Term ctx ty₁ → Term (.cons ty₁ ctx) ty₂ → Term ctx ty₂
+
+def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote
+  | .var h,     env => env.get h
+  | .const n,   _   => n
+  | .plus a b,  env => a.denote env + b.denote env
+  -- the following recursive call is interesting: Here the `ty.denote` for `f`'s type
+  -- becomes a function, and thus the recursive call takes an extra argument
+  -- But in the induction principle, we have `motive f` here, which does not
+  -- take an extra argument, so we have to be careful to not pass too many arguments to it
+  | .app f a,   env => f.denote env (a.denote env)
+  | .lam b,     env => fun x => b.denote (.cons x env)
+  | .let a b,   env => b.denote (.cons (a.denote env) env)
+
+derive_functional_induction Term.denote
+
+/--
+info: Term.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Prop)
+  (case1 : ∀ (a : List Ty) (ty : Ty) (h : Member ty a) (env : HList Ty.denote a), motive (Term.var h) env)
+  (case2 : ∀ (a : List Ty) (n : Nat) (x : HList Ty.denote a), motive (Term.const n) x)
+  (case3 :
+    ∀ (a : List Ty) (a_1 b : Term a Ty.nat) (env : HList Ty.denote a),
+      motive a_1 env → motive b env → motive (a_1.plus b) env)
+  (case4 :
+    ∀ (a : List Ty) (ty dom : Ty) (f : Term a (dom.fn ty)) (a_1 : Term a dom) (env : HList Ty.denote a),
+      motive a_1 env → motive f env → motive (f.app a_1) env)
+  (case5 :
+    ∀ (a : List Ty) (dom ran : Ty) (b : Term (dom :: a) ran) (env : HList Ty.denote a),
+      (∀ (x : dom.denote), motive b (HList.cons x env)) → motive b.lam env)
+  (case6 :
+    ∀ (a : List Ty) (ty ty₁ : Ty) (a_1 : Term a ty₁) (b : Term (ty₁ :: a) ty) (env : HList Ty.denote a),
+      motive a_1 env → motive b (HList.cons (a_1.denote env) env) → motive (a_1.let b) env)
+  {ctx : List Ty} {ty : Ty} : ∀ (a : Term ctx ty) (a_1 : HList Ty.denote ctx), motive a a_1
+-/
+#guard_msgs in
+#check Term.denote.induct
+
+end Term
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 88344d4cbc..0ca606cc95 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -11,8 +11,8 @@ derive_functional_induction ackermann
 /--
 info: Unary.ackermann.induct (motive : Nat × Nat → Prop) (case1 : ∀ (m : Nat), motive (0, m))
   (case2 : ∀ (n : Nat), motive (n, 1) → motive (n.succ, 0))
-  (case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (n.succ, m.succ))
-  (x : Nat × Nat) : motive x
+  (case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (n.succ, m.succ)) :
+  ∀ (a : Nat × Nat), motive a
 -/
 #guard_msgs in
 #check ackermann.induct
@@ -49,7 +49,7 @@ derive_functional_induction Tree.rev
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
-  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (x : Tree) : motive x
+  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a
 -/
 #guard_msgs in
 #check Tree.rev.induct
@@ -64,7 +64,7 @@ termination_by n => n
 derive_functional_induction fib
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check fib.induct
@@ -79,8 +79,8 @@ termination_by n => n
 derive_functional_induction have_tailrec
 
 /--
-info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ)
-  (x : Nat) : motive x
+info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
+  (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check have_tailrec.induct
@@ -96,8 +96,8 @@ termination_by n => n
 derive_functional_induction have_non_tailrec
 
 /--
-info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
-  (x : Nat) : motive x
+info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check have_non_tailrec.induct
@@ -116,8 +116,8 @@ info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 :
     ∀ (n : Nat),
       let h2 := ⋯;
-      motive n → motive n.succ)
-  (x : Nat) : motive x
+      motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check let_tailrec.induct
@@ -133,8 +133,8 @@ termination_by n => n
 derive_functional_induction let_non_tailrec
 
 /--
-info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
-  (x : Nat) : motive x
+info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check let_non_tailrec.induct
@@ -154,7 +154,7 @@ derive_functional_induction with_ite_tailrec
 /--
 info: with_ite_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
-  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_ite_tailrec.induct
@@ -175,7 +175,7 @@ derive_functional_induction with_ite_non_tailrec
 
 /--
 info: with_ite_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive n.succ.succ) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive n.succ.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_ite_non_tailrec.induct
@@ -191,9 +191,8 @@ termination_by n
 derive_functional_induction with_dite_non_tailrec
 
 /--
-info: with_dite_non_tailrec.induct (motive : Nat → Prop)
-(case1 : ∀ (x : Nat), (x - 1 < x → motive (x - 1)) → motive x)
-  (x : Nat) : motive x
+info: with_dite_non_tailrec.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (x - 1 < x → motive (x - 1)) → motive x)
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check with_dite_non_tailrec.induct
@@ -208,9 +207,8 @@ termination_by n
 derive_functional_induction with_dite_tailrec
 
 /--
-info: with_dite_tailrec.induct (motive : Nat → Prop)
-(case1 : ∀ (x : Nat), x - 1 < x → motive (x - 1) → motive x)
-  (case2 : ∀ (x : Nat), ¬x - 1 < x → motive x) (x : Nat) : motive x
+info: with_dite_tailrec.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), x - 1 < x → motive (x - 1) → motive x)
+  (case2 : ∀ (x : Nat), ¬x - 1 < x → motive x) (n : Nat) : motive n
 -/
 #guard_msgs in
 #check with_dite_tailrec.induct
@@ -227,7 +225,7 @@ derive_functional_induction with_match_refining_tailrec
 
 /--
 info: with_match_refining_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 0 → motive (Nat.succ 0))
-  (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) (x : Nat) : motive x
+  (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_match_refining_tailrec.induct
@@ -278,7 +276,7 @@ derive_functional_induction with_other_match_tailrec
 /--
 info: with_other_match_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
-  (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive n.succ) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_other_match_tailrec.induct
@@ -331,8 +329,8 @@ termination_by n => n
 derive_functional_induction with_match_non_tailrec
 
 /--
-info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
-  (x : Nat) : motive x
+info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_match_non_tailrec.induct
@@ -355,8 +353,8 @@ info: with_match_non_tailrec_refining.induct (motive : Nat → Prop) (case1 : mo
       (match n with
         | 0 => motive 0
         | m => motive m) →
-        motive n.succ)
-  (x : Nat) : motive x
+        motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_match_non_tailrec_refining.induct
@@ -373,8 +371,8 @@ derive_functional_induction with_overlap
 
 /--
 info: with_overlap.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) (case3 : motive 2) (case4 : motive 3)
-  (case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive n.succ) (x : Nat) :
-  motive x
+  (case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_overlap.induct
@@ -392,7 +390,7 @@ derive_functional_induction unary
 
 /--
 info: UnusedExtraParams.unary.induct (base : Nat) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x
+  (case2 : ∀ (n : Nat), motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check unary.induct
@@ -443,7 +441,7 @@ info: NonTailrecMatch.match_non_tail.induct (motive : Nat → Prop)
         | 1 => True
         | n.succ.succ => motive n ∧ motive (n + 1)) →
         motive x)
-  (x : Nat) : motive x
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check match_non_tail.induct
@@ -469,7 +467,7 @@ derive_functional_induction foo
 
 /--
 info: AsPattern.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
-  (x : Nat) : motive x
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check foo.induct
@@ -492,7 +490,7 @@ info: AsPattern.bar.induct (motive : Nat → Prop)
         | 0 => True
         | x@h:n.succ => motive n) →
         motive x)
-  (x : Nat) : motive x
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check bar.induct
@@ -526,7 +524,7 @@ decreasing_by
 derive_functional_induction foo
 /--
 info: GramSchmidt.foo.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (∀ (i : Nat), below x i → motive i) → motive x)
-  (x : Nat) : motive x
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check foo.induct
@@ -544,7 +542,7 @@ termination_by xs => xs
 derive_functional_induction foo
 /--
 info: LetFun.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (x : List α), motive x
+  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
 -/
 #guard_msgs in
 #check foo.induct
@@ -560,7 +558,7 @@ termination_by xs => xs
 derive_functional_induction bar
 /--
 info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (x : List α), motive x
+  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
 -/
 #guard_msgs in
 #check bar.induct
@@ -579,12 +577,13 @@ derive_functional_induction foo
 /--
 info: RecCallInDisrs.foo.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), foo n = 0 → motive n → motive n.succ)
-  (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check foo.induct
 
 
+set_option linter.unusedVariables false in
 def bar : Nat → Nat
   | 0 => 0
   | n+1 => match _h : n, bar n with
@@ -597,7 +596,7 @@ derive_functional_induction bar
 /--
 info: RecCallInDisrs.bar.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : bar 0 = 0 → motive 0 → motive (Nat.succ 0))
   (case3 : (bar 0 = 0 → False) → motive 0 → motive (Nat.succ 0))
-  (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) (x : Nat) : motive x
+  (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check bar.induct
@@ -679,7 +678,7 @@ derive_functional_induction unary
 
 /--
 info: DefaultArgument.unary.induct (fixed : Bool) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x
+  (case2 : ∀ (n : Nat), motive n → motive n.succ) (n : Nat) : motive n
 -/
 #guard_msgs in
 #check unary.induct
@@ -745,7 +744,7 @@ info: Dite.foo.induct (motive : Nat → Prop)
     ∀ (x : Nat),
       let j := x - 1;
       ¬j < x → motive x)
-  (x : Nat) : motive x
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check foo.induct
@@ -824,11 +823,11 @@ where
   termination_by as.size - i
 
 /--
-error: Function Errors.takeWhile does not look like a function defined by well-founded recursion.
+error: Function Errors.takeWhile does not look like a function defined by recursion.
 NB: If Errors.takeWhile is not itself recursive, but contains an inner recursive function (via `let rec` or `where`), try `Errors.takeWhile.go` where `go` is name of the inner function.
 -/
 #guard_msgs in
-derive_functional_induction takeWhile -- Cryptic error message
+derive_functional_induction takeWhile
 
 derive_functional_induction takeWhile.foo
 
@@ -853,7 +852,7 @@ derive_functional_induction foo
 /--
 info: PreserveParams.foo.induct (a : Nat) (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), a = 23 → motive n.succ) (case3 : ¬a = 23 → motive a.succ)
-  (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) (x : Nat) : motive x
+  (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check foo.induct