From 3d1d8fc1de632aedcd4a4e04404b949ac8572380 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 29 Apr 2025 18:43:06 +0200
Subject: [PATCH] feat: unfolding functional induction principles (#8088)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds the “unfolding” variant of the functional induction and
functional cases principles, under the name `foo.induct_unfolding` resp.
`foo.fun_cases_unfolding`. These theorems combine induction over the
structure of a recursive function with the unfolding of that function,
and should be more reliable, easier to use and more efficient than just
case-splitting and then rewriting with equational theorems.

For example  instead of
```
ackermann.induct
  (motive : Nat → Nat → Prop)
  (case1 : ∀ (m : Nat), motive 0 m)
  (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
  (x x : Nat) : motive x x
```
one gets
```
ackermann.fun_cases_unfolding
  (motive : Nat → Nat → Nat → Prop)
  (case1 : ∀ (m : Nat), motive 0 m (m + 1))
  (case2 : ∀ (n : Nat), motive n.succ 0 (ackermann n 1))
  (case3 : ∀ (n m : Nat), motive n.succ m.succ (ackermann n (ackermann (n + 1) m)))
  (x✝ x✝¹ : Nat) : motive x✝ x✝¹ (ackermann x✝ x✝¹)
```
---
 src/Lean/Elab/PreDefinition/Eqns.lean         |  25 -
 src/Lean/Elab/PreDefinition/Mutual.lean       |   4 +
 .../Elab/PreDefinition/Structural/Eqns.lean   |  27 +-
 src/Lean/Meta/ArgsPacker.lean                 |  55 +-
 src/Lean/Meta/Tactic/FunInd.lean              | 348 ++++++++++---
 src/Lean/Meta/Tactic/FunIndInfo.lean          |  21 +-
 src/Lean/Meta/Tactic/Simp/Types.lean          |  23 +
 tests/lean/run/funind_structural.lean         |   4 +-
 tests/lean/run/funind_unfolding.lean          | 487 ++++++++++++++++++
 tests/lean/run/funinduction_generalize.lean   |  44 +-
 10 files changed, 880 insertions(+), 158 deletions(-)
 create mode 100644 tests/lean/run/funind_unfolding.lean

diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 7b2b17599b..6d2c8f3d59 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -469,31 +469,6 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
     throwError "failed to generate unfold theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
   go mvarId
 
-/-- Generate the "unfold" lemma for `declName`. -/
-def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := do
-  let name := Name.str declName unfoldThmSuffix
-  realizeConst declName name (doRealize name)
-  return name
-where
-  doRealize name := withOptions (tactic.hygienic.set · false) do
-    lambdaTelescope info.value fun xs body => do
-      let us := info.levelParams.map mkLevelParam
-      let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
-      let goal ← mkFreshExprSyntheticOpaqueMVar type
-      mkUnfoldProof declName goal.mvarId!
-      let type ← mkForallFVars xs type
-      let value ← mkLambdaFVars xs (← instantiateMVars goal)
-      addDecl <| Declaration.thmDecl {
-        name, type, value
-        levelParams := info.levelParams
-      }
-
-def getUnfoldFor? (declName : Name) (getInfo? : Unit → Option EqnInfoCore) : MetaM (Option Name) := do
-  if let some info := getInfo? () then
-    return some (← mkUnfoldEq declName info)
-  else
-    return none
-
 builtin_initialize
   registerTraceClass `Elab.definition.unfoldEqn
   registerTraceClass `Elab.definition.eqns
diff --git a/src/Lean/Elab/PreDefinition/Mutual.lean b/src/Lean/Elab/PreDefinition/Mutual.lean
index 09e1d26ccd..6b150ff011 100644
--- a/src/Lean/Elab/PreDefinition/Mutual.lean
+++ b/src/Lean/Elab/PreDefinition/Mutual.lean
@@ -63,8 +63,12 @@ Assign final attributes to the definitions. Assumes the EqnInfos to be already p
 def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
   for preDef in preDefs do
     markAsRecursive preDef.declName
+  for preDef in preDefs.reverse do
     -- must happen before `generateEagerEqns`
+    -- must happen in reverse order so that constants realized as part of the first decl
+    -- have realizations for the other ones enabled
     enableRealizationsForConst preDef.declName
+  for preDef in preDefs do
     generateEagerEqns preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
     -- Unless the user asks for something else, mark the definition as irreducible
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index a9fd1dfca7..ba4af93792 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -77,7 +77,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added
-    realizeConst baseName name (doRealize name type)
+    realizeConst info.declNames[0]! name (doRealize name type)
   return thmNames
 where
   doRealize name type := withOptions (tactic.hygienic.set · false) do
@@ -102,9 +102,30 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   else
     return none
 
+/-- Generate the "unfold" lemma for `declName`. -/
+def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
+  let name := Name.str declName unfoldThmSuffix
+  realizeConst info.declNames[0]! name (doRealize name)
+  return name
+where
+  doRealize name := withOptions (tactic.hygienic.set · false) do
+    lambdaTelescope info.value fun xs body => do
+      let us := info.levelParams.map mkLevelParam
+      let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
+      let goal ← mkFreshExprSyntheticOpaqueMVar type
+      mkUnfoldProof declName goal.mvarId!
+      let type ← mkForallFVars xs type
+      let value ← mkLambdaFVars xs (← instantiateMVars goal)
+      addDecl <| Declaration.thmDecl {
+        name, type, value
+        levelParams := info.levelParams
+      }
+
 def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
-  let env ← getEnv
-  Eqns.getUnfoldFor? declName fun _ => eqnInfoExt.find? env declName |>.map (·.toEqnInfoCore)
+  if let some info := eqnInfoExt.find? (← getEnv) declName then
+    return some (← mkUnfoldEq declName info)
+  else
+    return none
 
 @[export lean_get_structural_rec_arg_pos]
 def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do
diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean
index 22c067cc79..60fea87e60 100644
--- a/src/Lean/Meta/ArgsPacker.lean
+++ b/src/Lean/Meta/ArgsPacker.lean
@@ -176,22 +176,32 @@ def uncurry (varNames : Array Name) (e : Expr) : MetaM Expr := do
       let value ← casesOn varNames.toList x u codomain e
       mkLambdaFVars #[x] value
 
-/-- Given `(A ⊗' B ⊗' … ⊗' D) → R` (non-dependent) `R`, return `A → B → … → D → R` -/
+/--
+Given type `(x : A ⊗' B ⊗' … ⊗' D) → R[x]`
+return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)]`
+-/
 private def curryType (varNames : Array Name) (type : Expr) : MetaM Expr := do
-  let some (domain, codomain) := type.arrow? |
-    throwError "curryType: Expected arrow type, got {type}"
-  go codomain varNames.toList domain
+  unless type.isForall do
+    throwError "curryType: Expected forall type, got {type}"
+  let packedDomain := type.bindingDomain!
+  go packedDomain packedDomain #[] varNames.toList
 where
-  go  (codomain : Expr) : List Name → Expr → MetaM Expr
-  | [], _ => pure codomain
-  | [_], domain => mkArrow domain codomain
-  | n::ns, domain =>
+  go (packedDomain domain : Expr) args : List Name → MetaM Expr
+  | [] => do
+      let packedArg := Unary.pack packedDomain args
+      instantiateForall type #[packedArg]
+  | [n] => do
+    withLocalDeclD n domain fun x => do
+      let dummy := Expr.const ``Unit []
+      mkForallFVars #[x] (← go packedDomain dummy (args.push x) [])
+  | n :: ns =>
     match_expr domain with
     | PSigma a b =>
-      withLocalDecl n .default a fun x => do
-        mkForallFVars #[x] (← go codomain ns (b.beta #[x]))
+      withLocalDeclD n a fun x => do
+        mkForallFVars #[x] (← go packedDomain (b.beta #[x]) (args.push x) ns)
     | _ => throwError "curryType: Expected PSigma type, got {domain}"
 
+
 /--
 Given expression `e` of type `(x : A ⊗' B ⊗' … ⊗' D) → R[x]`
 return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)]`
@@ -420,16 +430,19 @@ def uncurryND (es : Array Expr) : MetaM Expr := do
     mkLambdaFVars #[x] value
 
 /-
-Given type `(A ⊕' C) → R` (non-depenent), return types
+Given type `(A ⊕' C) → R` (possibly depenent), return types
 ```
 #[A → R, B → R]
 ```
 -/
 def curryType (n : Nat) (type : Expr) : MetaM (Array Expr) := do
-  let some (domain, codomain) := type.arrow? |
-    throwError "curryType: Expected arrow type, got {type}"
+  unless type.isForall do
+    throwError "curryType: Expected forall type, got {type}"
+  let domain := type.bindingDomain!
   let ds ← unpackType n domain
-  ds.toArray.mapM (fun d => mkArrow d codomain)
+  ds.toArray.mapIdxM fun i d =>
+    withLocalDeclD `x d fun x => do
+      mkForallFVars #[x] (← instantiateForall type #[← pack ds.length domain i x])
 
 end Mutual
 
@@ -528,7 +541,7 @@ def curryProj (argsPacker : ArgsPacker) (e : Expr) (i : Nat) : MetaM Expr := do
 
 
 /--
-Given type `(x : a ⊗' b ⊕' c ⊗' d) → R` (non-dependent), return types
+Given type `(x : a ⊗' b ⊕' c ⊗' d) → R` (dependent), return types
 ```
 #[(x: a) → (y : b) → R, (x : c) → (y : d) → R]
 ```
@@ -569,9 +582,9 @@ where
 /--
 Given `value : type` where `type` is
 ```
-(m : a ⊗' b ⊕' c ⊗' d → s) → r[m]
+(m : (x : a ⊗' b ⊕' c ⊗' d) → s[x]) → r[m]
 ```
-brings `m1 : a → b → s` and `m2 : c → d → s` into scope. The continuation receives
+brings `m1 : (x : a) → (y : b) → s[.inl ⟨x,y⟩]` and `m2 : (x : c) → (y : d) → s[.inr ⟨x,y⟩]` into scope. The continuation receives
 
  * FVars for `m1`…
  * `e[m]`
@@ -585,14 +598,14 @@ unless `numFuns = 1`
 def curryParam {α} (argsPacker : ArgsPacker) (value : Expr) (type : Expr)
     (k : Array Expr → Expr → Expr → MetaM α) : MetaM α := do
   unless type.isForall do
-    throwError "uncurryParam: expected forall, got {type}"
+    throwError "curryParam: expected forall, got {type}"
   let packedMotiveType := type.bindingDomain!
-  unless packedMotiveType.isArrow do
-    throwError "uncurryParam: unexpected packed motive {packedMotiveType}"
+  unless packedMotiveType.isForall do
+    throwError "curryParam: unexpected packed motive, not a forall{indentExpr packedMotiveType}"
   -- Bring unpacked motives (motive1 : a → b → Prop and motive2 : c → d → Prop) into scope
   withCurriedDecl argsPacker type.bindingName! packedMotiveType fun motives => do
     -- Combine them into a packed motive (motive : a ⊗' b ⊕' c ⊗' d → Prop), and use that
-    let motive ← argsPacker.uncurryND motives
+    let motive ← argsPacker.uncurryWithType packedMotiveType motives
     let type ← instantiateForall type #[motive]
     let value := mkApp value motive
     k motives value type
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index f45ba69dc4..0006fe3de3 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -175,6 +175,32 @@ differences:
 
 * The elaboration of structurally recursive function can handle extra arguments. We keep the
   `motive` parameters in the original order.
+
+## Unfolding principles
+
+The code can also create a variant of the induction/cases principles that automatially unfolds
+the function application. It's motive abstracts over the function call, so for the ackermann
+function one gets
+
+```
+ackermann.fun_cases_unfolding
+  (motive : Nat → Nat → Nat → Prop)
+  (case1 : ∀ (m : Nat), motive 0 m (m + 1))
+  (case2 : ∀ (n : Nat), motive n.succ 0 (ackermann n 1))
+  (case3 : ∀ (n m : Nat), motive n.succ m.succ (ackermann n (ackermann (n + 1) m)))
+  (x✝ x✝¹ : Nat) : motive x✝ x✝¹ (ackermann x✝ x✝¹)
+```
+
+To implement this, in the inital goal `motive x (ackermann x)` of `buildInductionBody` we unfold the
+function definition, and then reduce is as we go into match, ite or let expressions, using the
+`withRewrittenMotive` function.
+
+This gives us great control over the reduction, for example to move `let` expressions to the context
+simultaneously.
+
+The combinators passed to `withRewrittenMotive` are forgiving, so when `unfolding := false`, or when
+something goes wrong, one still gets a useful induction principle, just maybe with the function
+not fully simplified.
 -/
 
 set_option autoImplicit false
@@ -382,7 +408,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
       assert! fvar == oldIH
       pure <| mkFVar newIH
 
-    -- Now see if the type o/--f the expression we are building is a motive application.
+    -- Now see if the type of the expression we are building is a motive application.
     -- If it is we want to replace it with the corresponding function application,
     -- and remember the expression as a IH to be used in an inductive case.
 
@@ -528,6 +554,120 @@ def maskArray {α} (mask : Array Bool) (xs : Array α) : Array α := Id.run do
   return ys
 
 /--
+Applies `rw` to `goal`, passes the rewritten `goal'` to `k` (which should return an expression of
+type `goal'`), and wraps that using the proof from `rw`.
+-/
+def withRewrittenMotive (goal : Expr) (rw : Expr → MetaM Simp.Result) (k : Expr → M2 Expr) : M2 Expr := do
+  let r ← rw goal
+  let e ← k r.expr
+  r.mkEqMPR e
+
+def inLastArg (rw : Expr → MetaM Simp.Result) (goal : Expr) : MetaM Simp.Result := do
+  match goal with
+  | .app goalFn arg =>
+    let r ← rw arg
+    Simp.mkCongrArg goalFn r
+  | _ =>
+    return { expr := goal }
+
+/--
+If `goal` is of the form `motive a b e`, applies `rw` to `e`, passes the simplified
+`goal'` to `k` (which should return an expression of type `goal'`), and rewrites that term
+accordingly.
+-/
+def withRewrittenMotiveArg (goal : Expr) (rw : Expr → MetaM Simp.Result) (k : Expr → M2 Expr) : M2 Expr := do
+  withRewrittenMotive goal (inLastArg rw) k
+
+/--
+Use to write inside the packed motives used for mutual structural recursion.
+-/
+partial def inProdLambdaLastArg (rw : Expr → MetaM Simp.Result) (goal : Expr) : MetaM Simp.Result := do
+  match_expr goal with
+  | PProd.mk _ _ goal1 goal2 =>
+    let r1 ← inProdLambdaLastArg rw goal1
+    let r2 ← inProdLambdaLastArg rw goal2
+    let f := goal.appFn!.appFn!
+    Simp.mkCongr (← Simp.mkCongrArg f r1) r2
+  | _ =>
+    lambdaTelescope goal fun xs goal => do
+      let r ← inLastArg rw goal
+      r.addLambdas xs
+
+def rwIfWith (hc : Expr) (e : Expr) : MetaM Simp.Result := do
+  match_expr e with
+  | ite@ite α c h t f =>
+    let us := ite.constLevels!
+    if (← isDefEq c (← inferType hc)) then
+      return {
+        expr := t
+        proof? := (mkAppN (mkConst ``if_pos us) #[c, h, hc, α, t, f])
+      }
+    if (← isDefEq (mkNot c) (← inferType hc)) then
+      return {
+        expr := f
+        proof? := (mkAppN (mkConst ``if_neg us) #[c, h, hc, α, t, f])
+      }
+    else
+      return { expr := e}
+  | dite@dite α c h t f =>
+    let us := dite.constLevels!
+    if (← isDefEq c (← inferType hc)) then
+      return {
+        expr := t.beta #[hc]
+        proof? := (mkAppN (mkConst ``dif_pos us) #[c, h, hc, α, t, f])
+      }
+    if (← isDefEq (mkNot c) (← inferType hc)) then
+      return {
+        expr := f.beta #[hc]
+        proof? := (mkAppN (mkConst ``dif_neg us) #[c, h, hc, α, t, f])
+      }
+    else
+      return { expr := e }
+  | _ =>
+      return { expr := e }
+
+def rwLetWith (h : Expr) (e : Expr) : MetaM Simp.Result := do
+  if e.isLet then
+    if (← isDefEq e.letValue! h) then
+      return { expr := e.letBody!.instantiate1 h }
+  return { expr := e }
+
+def rwHaveWith (h : Expr) (e : Expr) : MetaM Simp.Result := do
+  if let some (_n, t, _v, b) := e.letFun? then
+    if (← isDefEq t (← inferType h)) then
+      return { expr := b.instantiate1 h }
+  return { expr := e }
+
+def rwFun (names : Array Name) (e : Expr) : MetaM Simp.Result := do
+  e.withApp fun f xs => do
+    if let some name := names.find? f.isConstOf then
+      let some unfoldThm ← getUnfoldEqnFor? name (nonRec := true)
+        | return { expr := e }
+      let h := mkAppN (mkConst unfoldThm f.constLevels!) xs
+      let some (_, _, rhs) := (← inferType h).eq?
+        | throwError "Not an equality: {h}"
+      return { expr := rhs, proof? := h }
+    else
+      return { expr := e }
+
+def rwMatcher (e : Expr) : MetaM Simp.Result := do
+  if e.isAppOf ``PSum.casesOn || e.isAppOf ``PSigma.casesOn then
+    let mut e := e
+    while true do
+      if let some e' ← reduceRecMatcher? e then
+          e := e'.headBeta
+      else
+        let e' := e.headBeta
+        if e != e' then
+          e := e'
+        else
+          break
+    return { expr := e }
+  else
+    Split.simpMatch e
+
+/--
+
 Builds an expression of type `goal` by replicating the expression `e` into its tail-call-positions,
 where it calls `buildInductionCase`. Collects the cases of the final induction hypothesis
 as `MVars` as it goes.
@@ -543,10 +683,12 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
     let c' ← foldAndCollect oldIH newIH isRecCall c
     let h' ← foldAndCollect oldIH newIH isRecCall h
     let t' ← withLocalDecl `h .default c' fun h => M2.branch do
-      let t' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall t
+      let t' ← withRewrittenMotiveArg goal (rwIfWith h) fun goal' =>
+        buildInductionBody toErase toClear goal' oldIH newIH isRecCall t
       mkLambdaFVars #[h] t'
     let f' ← withLocalDecl `h .default (mkNot c') fun h => M2.branch do
-      let f' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall f
+      let f' ← withRewrittenMotiveArg goal (rwIfWith h) fun goal' =>
+        buildInductionBody toErase toClear goal' oldIH newIH isRecCall f
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
@@ -555,11 +697,13 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
     let h' ← foldAndCollect oldIH newIH isRecCall h
     let t' ← withLocalDecl `h .default c' fun h => M2.branch do
       let t ← instantiateLambda t #[h]
-      let t' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall t
+      let t' ← withRewrittenMotiveArg goal (rwIfWith h) fun goal' =>
+        buildInductionBody toErase toClear goal' oldIH newIH isRecCall t
       mkLambdaFVars #[h] t'
     let f' ← withLocalDecl `h .default (mkNot c') fun h => M2.branch do
       let f ← instantiateLambda f #[h]
-      let f' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall f
+      let f' ← withRewrittenMotiveArg goal (rwIfWith h) fun goal' =>
+        buildInductionBody toErase toClear goal' oldIH newIH isRecCall f
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
@@ -608,7 +752,9 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
               let #[newIH'] := newIH' | unreachable!
               let toErase' := toErase ++ #[oldIH', newIH'.fvarId!]
               let toClear' := toClear ++ matcherApp.discrs.filterMap (·.fvarId?)
-              let alt' ← buildInductionBody toErase' toClear'  goal' oldIH' newIH'.fvarId! isRecCall alt
+              let alt' ← withRewrittenMotiveArg goal' rwMatcher fun goal'' => do
+                -- logInfo m!"rwMatcher after {matcherApp.matcherName} on{indentExpr goal'}\nyields{indentExpr goal''}"
+                buildInductionBody toErase' toClear' goal'' oldIH' newIH'.fvarId! isRecCall alt
               mkLambdaFVars #[newIH'] alt')
         (onRemaining := fun _ => pure #[.fvar newIH])
       return matcherApp'.toExpr
@@ -624,7 +770,8 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
         (onParams := (foldAndCollect oldIH newIH isRecCall ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => M2.branch do
-          buildInductionBody toErase toClear expAltType oldIH newIH isRecCall alt)
+          withRewrittenMotiveArg expAltType Split.simpMatch fun expAltType' =>
+            buildInductionBody toErase toClear expAltType' oldIH newIH isRecCall alt)
       return matcherApp'.toExpr
 
   -- we look through mdata
@@ -636,14 +783,16 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
     return ← withLetDecl n t' v' fun x => M2.branch do
-      let b' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall (b.instantiate1 x)
+      let b' ← withRewrittenMotiveArg goal (rwLetWith x) fun goal' =>
+        buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
       mkLetFVars #[x] b'
 
   if let some (n, t, v, b) := e.letFun? then
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
     return ← withLocalDeclD n t' fun x => M2.branch do
-      let b' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall (b.instantiate1 x)
+      let b' ← withRewrittenMotiveArg goal (rwHaveWith x) fun goal' =>
+        buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
       mkLetFun x v' b'
 
   -- Special case for traversing the PProd’ed bodies in our encoding of structural mutual recursion
@@ -696,8 +845,8 @@ def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : M
 Given a unary definition `foo` defined via `WellFounded.fixF`, derive a suitable induction principle
 `foo.induct` for it. See module doc for details.
  -/
-def deriveUnaryInduction (name : Name) : MetaM Name := do
-  let inductName := getFunInductName name
+def deriveUnaryInduction (unfolding : Bool) (name : Name) : MetaM Name := do
+  let inductName := getFunInductName (unfolding := unfolding) name
   realizeConst name inductName (doRealize inductName)
   return inductName
 where doRealize (inductName : Name) := do
@@ -721,17 +870,29 @@ where doRealize (inductName : Name) := do
       unless params.back! == target do
         throwError "functional induction: expected the target as last parameter{indentExpr e}"
       let fixedParamPerms := params.pop
-      let motiveType ← mkForallFVars #[target] (.sort levelZero)
+      let motiveType ←
+        if unfolding then
+          withLocalDeclD `r (← instantiateForall info.type params) fun r =>
+            mkForallFVars #[target, r] (.sort 0)
+        else
+          mkForallFVars #[target] (.sort 0)
       withLocalDeclD `motive motiveType fun motive => do
         let fn := mkAppN (← mkConstWithLevelParams name) fixedParamPerms
         let isRecCall : Expr → Option Expr := fun e =>
-          if e.isApp && e.appFn!.isFVarOf motive.fvarId! then
-            mkApp fn e.appArg!
+          e.withApp fun f xs =>
+            if f.isFVarOf motive.fvarId! && xs.size > 0 then
+            mkApp fn xs[0]!
           else
             none
 
+        let motiveArg ←
+          if unfolding then
+            let motiveArg := mkApp2 motive target (mkAppN (← mkConstWithLevelParams name) params)
+            mkLambdaFVars #[target] motiveArg
+          else
+            pure motive
         let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
-        let e' := mkApp4 e' α motive rel wf
+        let e' := mkApp4 e' α motiveArg rel wf
         check e'
         let (body', mvars) ← M2.run do
           forallTelescope (← inferType e').bindingDomain! fun xs goal => do
@@ -744,7 +905,8 @@ where doRealize (inductName : Name) := do
             let body ← instantiateLambda body targets
             lambdaTelescope1 body fun oldIH body => do
               let body ← instantiateLambda body extraParams
-              let body' ← buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
+              let body' ← withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
+                buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall 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')
@@ -792,10 +954,10 @@ where doRealize (inductName : Name) := do
 Given a realizer for `foo.mutual_induct`, defines `foo.induct`, `bar.induct` etc.
 Used for well-founded and structural recursion.
 -/
-def projectMutualInduct (names : Array Name) (mutualInduct : MetaM Name) (finalizeFirstInd : MetaM Unit) : MetaM Unit := do
+def projectMutualInduct (unfolding : Bool) (names : Array Name) (mutualInduct : MetaM Name) (finalizeFirstInd : MetaM Unit) : MetaM Unit := do
   for name in names, idx in [:names.size] do
-    let inductName := getFunInductName name
-    realizeConst name inductName do
+    let inductName := getFunInductName (unfolding := unfolding) name
+    realizeConst names[0]! inductName do
       let ci ← getConstInfo (← mutualInduct)
       let levelParams := ci.levelParams
       let value ← forallTelescope ci.type fun xs _body => do
@@ -812,9 +974,9 @@ def projectMutualInduct (names : Array Name) (mutualInduct : MetaM Name) (finali
 For a (non-mutual!) definition of `name`, uses the `FunIndInfo` associated with the `unaryInduct` and
 derives the one for the n-ary function.
 -/
-def setNaryFunIndInfo (fixedParamPerms : FixedParamPerms) (name : Name) (unaryInduct : Name) : MetaM Unit := do
+def setNaryFunIndInfo (unfolding : Bool) (fixedParamPerms : FixedParamPerms) (name : Name) (unaryInduct : Name) : MetaM Unit := do
   assert!  fixedParamPerms.perms.size = 1 -- only non-mutual for now
-  let funIndName := getFunInductName name
+  let funIndName := getFunInductName (unfolding := unfolding) name
   unless funIndName = unaryInduct do
     let some unaryFunIndInfo ← getFunIndInfoForInduct? unaryInduct
       | throwError "Expected {unaryInduct} to have FunIndInfo"
@@ -894,22 +1056,22 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
 Retrieves `foo._unary.induct`, where the motive is a `PSigma`/`PSum` type, and
 unpacks it into a n-ary and (possibly) joint induction principle.
 -/
-def unpackMutualInduction (eqnInfo : WF.EqnInfo) : MetaM Name := do
+def unpackMutualInduction (unfolding : Bool) (eqnInfo : WF.EqnInfo) : MetaM Name := do
   let inductName := if eqnInfo.declNames.size > 1 then
-    getMutualInductName eqnInfo.declNames[0]!
+    getMutualInductName (unfolding := unfolding) eqnInfo.declNames[0]!
   else
     -- If there is no mutual recursion, we generate the `foo.induct` directly.
-    getFunInductName eqnInfo.declNames[0]!
+    getFunInductName (unfolding := unfolding) eqnInfo.declNames[0]!
   realizeConst eqnInfo.declNames[0]! inductName (doRealize inductName)
   return inductName
 where doRealize inductName := do
-  let unaryInductName ← deriveUnaryInduction eqnInfo.declNameNonRec
+  let unaryInductName ← deriveUnaryInduction (unfolding := unfolding) eqnInfo.declNameNonRec
   mapError (f := (m!"Cannot unpack functional cases principle {.ofConstName unaryInductName} (please report this issue)\n{indentD ·}")) do
   let ci ← getConstInfo unaryInductName
   let us := ci.levelParams
   let value := .const ci.name (us.map mkLevelParam)
   let motivePos ← forallTelescope ci.type fun xs concl => concl.withApp fun motive targets => do
-    unless motive.isFVar && targets.size = 1 && targets.all (·.isFVar) do
+    unless motive.isFVar && targets.size = (if unfolding then 2 else 1) && targets[0]!.isFVar do
       throwError "conclusion {concl} does not look like a packed motive application"
     let packedTarget := targets[0]!
     unless xs.back! == packedTarget do
@@ -942,7 +1104,7 @@ where doRealize inductName := do
     { name := inductName, levelParams := ci.levelParams, type, value }
 
   if eqnInfo.argsPacker.numFuncs = 1 then
-    setNaryFunIndInfo eqnInfo.fixedParamPerms eqnInfo.declNames[0]! unaryInductName
+    setNaryFunIndInfo (unfolding := unfolding) eqnInfo.fixedParamPerms eqnInfo.declNames[0]! unaryInductName
 
 def withLetDecls {α} (name : Name) (ts : Array Expr) (es : Array Expr) (k : Array Expr → MetaM α) : MetaM α := do
   assert! es.size = ts.size
@@ -960,12 +1122,12 @@ Given a recursive definition `foo` defined via structural recursion, derive `foo
 if needed, and `foo.induct` for all functions in the group.
 See module doc for details.
  -/
-def deriveInductionStructural (names : Array Name) (fixedParamPerms : FixedParamPerms) : MetaM Name := do
+def deriveInductionStructural (unfolding : Bool) (names : Array Name) (fixedParamPerms : FixedParamPerms) : MetaM Name := do
   let inductName :=
     if names.size = 1 then
-      getFunInductName names[0]!
+      getFunInductName (unfolding := unfolding) names[0]!
     else
-      getMutualInductName names[0]!
+      getMutualInductName (unfolding := unfolding) names[0]!
   realizeConst names[0]! inductName (doRealize inductName)
   return inductName
 where doRealize inductName := do
@@ -1050,11 +1212,16 @@ where doRealize inductName := do
 
         -- Calculate the types of the induction motives (natural argument order) for each function
         let motiveTypes ← infos.mapIdxM fun funIdx info => do
-          lambdaTelescope (← fixedParamPerms.perms[funIdx]!.instantiateLambda info.value xs) fun ys _ =>
-            mkForallFVars ys (.sort levelZero)
-        let motiveArities ← infos.mapIdxM fun funIdx info => do
-          lambdaTelescope (← fixedParamPerms.perms[funIdx]!.instantiateLambda info.value xs) fun ys _ =>
-            pure ys.size
+          let funType ← fixedParamPerms.perms[funIdx]!.instantiateForall info.type xs
+          forallBoundedTelescope funType (some (fixedParamPerms.perms[funIdx]!.size - xs.size)) fun ys rType => do
+            if unfolding then
+              withLocalDeclD `r rType fun r =>
+                mkForallFVars (ys.push r) (.sort 0)
+            else
+              mkForallFVars ys (.sort 0)
+        trace[Meta.FunInd] m!"motiveTypes: {motiveTypes}"
+        let motiveArities ← motiveTypes.mapM fun motiveType =>
+          forallTelescope motiveType fun ys _ => pure ys.size
         let motiveNames := Array.ofFn (n := infos.size) fun ⟨i, _⟩ =>
           if infos.size = 1 then .mkSimple "motive" else .mkSimple s!"motive_{i+1}"
 
@@ -1065,15 +1232,27 @@ where doRealize inductName := do
             if let .some funIdx := motives.idxOf? e.getAppFn then
               if e.getAppNumArgs = motiveArities[funIdx]! then
                 let info := infos[funIdx]!
-                let args := fixedParamPerms.perms[funIdx]!.buildArgs xs e.getAppArgs
+                let args := if unfolding then e.getAppArgs.pop else e.getAppArgs
+                let args := fixedParamPerms.perms[funIdx]!.buildArgs xs args
                 return mkAppN (.const info.name (info.levelParams.map mkLevelParam)) args
             .none
 
-          -- Motives with parameters reordered, to put indices and major first
-          let brecMotives ← (Array.zip motives recArgInfos).mapM fun (motive, recArgInfo) => do
-            forallTelescope (← inferType motive) fun ys _ => do
+          -- Motives with parameters reordered, to put indices and major first,
+          -- and (when unfolding) the result field instantiated
+          let mut brecMotives := #[]
+          for motive in motives, recArgInfo in recArgInfos, info in infos, funIdx in [:motives.size] do
+            let brecMotive ← forallTelescope (← inferType motive) fun ys _ => do
+              let ys := if unfolding then ys.pop else ys
               let (indicesMajor, rest) := recArgInfo.pickIndicesMajor ys
-              mkLambdaFVars indicesMajor (← mkForallFVars rest (mkAppN motive ys))
+              let motiveArg := mkAppN motive ys
+              let motiveArg ← if unfolding then
+                let args := fixedParamPerms.perms[funIdx]!.buildArgs xs ys
+                let fnCall := mkAppN (.const info.name (info.levelParams.map mkLevelParam)) args
+                pure <| mkApp motiveArg fnCall
+              else
+                pure motiveArg
+              mkLambdaFVars indicesMajor (← mkForallFVars rest motiveArg)
+            brecMotives := brecMotives.push brecMotive
 
           -- We need to pack these motives according to the `positions` assignment.
           let packedMotives ← positions.mapMwith PProdN.packLambdas brecMotiveTypes brecMotives
@@ -1098,7 +1277,9 @@ where doRealize inductName := do
                 lambdaTelescope1 body fun oldIH body => do
                   trace[Meta.FunInd] "replacing {Expr.fvar oldIH} with {genIH}"
                   let body ← instantiateLambda body extraParams
-                  let body' ← buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
+                  let body' ←
+                    withRewrittenMotive goal (inProdLambdaLastArg (rwFun names)) fun goal' =>
+                      buildInductionBody #[oldIH, genIH.fvarId!] #[] goal' oldIH genIH.fvarId! isRecCall 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')
@@ -1188,39 +1369,44 @@ In the future, we might post-process the theorem (or run the code below iterativ
 targets that are unchanged in each case, so simplify applying the lemma when these “fixed” parameters
 are not variables, to avoid having to generalize them.
 -/
-def deriveCases (name : Name) : MetaM Unit := do
-  let casesName := getFunCasesName name
+def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do
+  let casesName := getFunCasesName (unfolding := unfolding) name
   realizeConst name casesName do
   mapError (f := (m!"Cannot derive functional cases principle (please report this issue)\n{indentD ·}")) do
     let info ← getConstInfo name
-    let value ←
-      if let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := false) name then
-        let eqInfo ← getConstInfo unfoldEqnName
-        forallTelescope eqInfo.type fun xs body => do
-          let some (_, _, rhs) := body.eq?
-            | throwError "Type of {unfoldEqnName} not an equality: {body}"
-          mkLambdaFVars xs rhs
-      else if let some value := info.value? then
-        pure value
-      else
-        throwError "'{name}' does not have an unfold theorem nor a value"
+    let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) name
+      | throwError "'{name}' does not have an unfold theorem nor a value"
+    let value ← do
+      let eqInfo ← getConstInfo unfoldEqnName
+      forallTelescope eqInfo.type fun xs body => do
+        let some (_, _, rhs) := body.eq?
+          | throwError "Type of {unfoldEqnName} not an equality: {body}"
+        mkLambdaFVars xs rhs
     let motiveType ← lambdaTelescope value fun xs _body => do
-      mkForallFVars xs (.sort 0)
+      if unfolding then
+        withLocalDeclD `r (← instantiateForall info.type xs) fun r =>
+          mkForallFVars (xs.push r) (.sort 0)
+      else
+        mkForallFVars xs (.sort 0)
     let motiveArity ← lambdaTelescope value fun xs _body => do
       pure xs.size
     let e' ← withLocalDeclD `motive motiveType fun motive => do
       lambdaTelescope value fun xs body => do
-        let (e',mvars) ← M2.run do
+        let (e', mvars) ← M2.run do
           let goal := mkAppN motive xs
-          -- We bring an unused FVars into scope to pass as `oldIH` and `newIH`. These do not appear anywhere
-          -- so `buildInductionBody` should just do the right thing
-          withLocalDeclD `fakeIH (mkConst ``Unit) fun fakeIH =>
-            let isRecCall := fun _ => none
-            buildInductionBody #[fakeIH.fvarId!] #[] goal fakeIH.fvarId! fakeIH.fvarId! isRecCall body
+          let goal ← if unfolding then
+            pure <| mkApp goal (mkAppN (← mkConstWithLevelParams name) xs)
+          else
+            pure goal
+          withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
+            -- We bring an unused FVars into scope to pass as `oldIH` and `newIH`. These do not appear anywhere
+            -- so `buildInductionBody` should just do the right thing
+            withLocalDeclD `fakeIH (mkConst ``Unit) fun fakeIH =>
+              let isRecCall := fun _ => none
+              buildInductionBody #[fakeIH.fvarId!] #[] goal fakeIH.fvarId! fakeIH.fvarId! isRecCall body
         let e' ← mkLambdaFVars xs e'
         let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
-        let e' ← mkLambdaFVars #[motive] e'
-        pure e'
+        mkLambdaFVars #[motive] e'
 
     unless (← isTypeCorrect e') do
       logError m!"constructed functional cases principle is not type correct:{indentExpr e'}"
@@ -1244,40 +1430,41 @@ def deriveCases (name : Name) : MetaM Unit := do
       params := .replicate motiveArity .target
     }
 
-
 /--
 Given a recursively defined function `foo`, derives `foo.induct`. See the module doc for details.
 -/
-def deriveInduction (name : Name) : MetaM Unit := do
+def deriveInduction (unfolding : Bool) (name : Name) : MetaM Unit := do
   mapError (f := (m!"Cannot derive functional induction principle (please report this issue)\n{indentD ·}")) do
     if let some eqnInfo := WF.eqnInfoExt.find? (← getEnv) name then
-      let unaryInductName ← deriveUnaryInduction eqnInfo.declNameNonRec
+      let unaryInductName ← deriveUnaryInduction unfolding eqnInfo.declNameNonRec
       if eqnInfo.declNames.size > 1 then
-        projectMutualInduct eqnInfo.declNames (unpackMutualInduction eqnInfo) do
+        projectMutualInduct unfolding eqnInfo.declNames (unpackMutualInduction unfolding eqnInfo) do
           -- We set the FunIndInfo on the first induction principle, which must happen inside its
           -- realization.
           if eqnInfo.argsPacker.numFuncs = 1 then
-            setNaryFunIndInfo eqnInfo.fixedParamPerms eqnInfo.declNames[0]! unaryInductName
+            setNaryFunIndInfo (unfolding := unfolding) eqnInfo.fixedParamPerms eqnInfo.declNames[0]! unaryInductName
       else
         -- (in this case, `unpackMutualInduction` already does `setNaryFunIndInfo`)
-        let _ ← unpackMutualInduction eqnInfo
+        let _ ← unpackMutualInduction unfolding eqnInfo
     else if let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) name then
       if eqnInfo.declNames.size > 1 then
-        projectMutualInduct eqnInfo.declNames (deriveInductionStructural eqnInfo.declNames eqnInfo.fixedParamPerms) (pure ())
+        projectMutualInduct unfolding eqnInfo.declNames (deriveInductionStructural unfolding eqnInfo.declNames eqnInfo.fixedParamPerms) (pure ())
       else
-        let _ ← deriveInductionStructural eqnInfo.declNames eqnInfo.fixedParamPerms
+        let _ ← deriveInductionStructural unfolding eqnInfo.declNames eqnInfo.fixedParamPerms
     else
       throwError "constant '{name}' is not structurally or well-founded recursive"
 
 def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
   let .str p s := name | return false
   match s with
-  | "induct" =>
+  | "induct"
+  | "induct_unfolding" =>
     if let some eqnInfo := WF.eqnInfoExt.find? env p then
       return true
     if (Structural.eqnInfoExt.find? env p).isSome then return true
     return false
-  | "mutual_induct" =>
+  | "mutual_induct"
+  | "mutual_induct_unfolding" =>
     if let some eqnInfo := WF.eqnInfoExt.find? env p then
       if h : eqnInfo.declNames.size > 1 then
         return eqnInfo.declNames[0] = p
@@ -1291,7 +1478,8 @@ def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
 def isFunCasesName (env : Environment) (name : Name) : Bool := Id.run do
   let .str p s := name | return false
   match s with
-  | "fun_cases" =>
+  | "fun_cases"
+  | "fun_cases_unfolding" =>
     if (WF.eqnInfoExt.find? env p).isSome then return true
     if (Structural.eqnInfoExt.find? env p).isSome then return true
     if let some ci := env.find? p then
@@ -1306,16 +1494,18 @@ builtin_initialize
 
   registerReservedNameAction fun name => do
     if isFunInductName (← getEnv) name then
-      let .str p _ := name | return false
-      MetaM.run' <| deriveInduction p
+      let .str p s := name | return false
+      let unfolding := s.endsWith "_unfolding"
+      MetaM.run' <| deriveInduction unfolding p
       return true
     if isFunCasesName (← getEnv) name then
-      let .str p _ := name | return false
-      MetaM.run' <| deriveCases p
+      let .str p s := name | return false
+      let unfolding := s == "fun_cases_unfolding"
+      MetaM.run' <| deriveCases unfolding p
       return true
     return false
 
 end Lean.Tactic.FunInd
 
- builtin_initialize
+builtin_initialize
    Lean.registerTraceClass `Meta.FunInd
diff --git a/src/Lean/Meta/Tactic/FunIndInfo.lean b/src/Lean/Meta/Tactic/FunIndInfo.lean
index 34f1dd8bad..2c37ec92b8 100644
--- a/src/Lean/Meta/Tactic/FunIndInfo.lean
+++ b/src/Lean/Meta/Tactic/FunIndInfo.lean
@@ -41,14 +41,23 @@ deriving Inhabited, Repr
 
 builtin_initialize funIndInfoExt : MapDeclarationExtension FunIndInfo ← mkMapDeclarationExtension
 
-def getFunInductName (declName : Name) : Name :=
-  declName ++ `induct
+def getFunInductName (declName : Name) (unfolding : Bool := false) : Name :=
+  if unfolding then
+    declName ++ `induct_unfolding
+  else
+    declName ++ `induct
 
-def getFunCasesName (declName : Name) : Name :=
-  declName ++ `fun_cases
+def getFunCasesName (declName : Name) (unfolding : Bool := false) : Name :=
+  if unfolding then
+    declName ++ `fun_cases_unfolding
+  else
+    declName ++ `fun_cases
 
-def getMutualInductName (declName : Name) : Name :=
-  declName ++ `mutual_induct
+def getMutualInductName (declName : Name) (unfolding : Bool := false) : Name :=
+  if unfolding then
+    declName ++ `mutual_induct_unfolding
+  else
+    declName ++ `mutual_induct
 
 def getFunInduct? (cases : Bool) (declName : Name) : CoreM (Option Name) := do
   let .defnInfo _ ← getConstInfo declName | return none
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 0273eb99cc..599fddd31a 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -534,11 +534,23 @@ def Result.getProof' (source : Expr) (r : Result) : MetaM Expr := do
 def Result.mkCast (r : Simp.Result) (e : Expr) : MetaM Expr := do
   mkAppM ``cast #[← r.getProof, e]
 
+/-- Construct the `Expr` `h.mpr e`, from a `Simp.Result` with proof `h`. -/
+def Result.mkEqMPR (r : Simp.Result) (e : Expr) : MetaM Expr := do
+  if r.proof?.isNone && r.expr == e then
+    pure e
+  else
+    Meta.mkEqMPR (← r.getProof) e
+
 def mkCongrFun (r : Result) (a : Expr) : MetaM Result :=
   match r.proof? with
   | none   => return { expr := mkApp r.expr a, proof? := none }
   | some h => return { expr := mkApp r.expr a, proof? := (← Meta.mkCongrFun h a) }
 
+def mkCongrArg (f : Expr) (r : Result) : MetaM Result :=
+  match r.proof? with
+  | none   => return { expr := mkApp f r.expr, proof? := none }
+  | some h => return { expr := mkApp f r.expr, proof? := (← Meta.mkCongrArg f h) }
+
 def mkCongr (r₁ r₂ : Result) : MetaM Result :=
   let e := mkApp r₁.expr r₂.expr
   match r₁.proof?, r₂.proof? with
@@ -773,6 +785,7 @@ def DStep.addExtraArgs (s : DStep) (extraArgs : Array Expr) : DStep :=
   | .continue (some eNew) => .continue (mkAppN eNew extraArgs)
 
 def Result.addLambdas (r : Result) (xs : Array Expr) : MetaM Result := do
+  if xs.isEmpty then return r
   let eNew ← mkLambdaFVars xs r.expr
   match r.proof? with
   | none   => return { expr := eNew }
@@ -781,6 +794,16 @@ def Result.addLambdas (r : Result) (xs : Array Expr) : MetaM Result := do
       mkFunExt (← mkLambdaFVars #[x] h)
     return { expr := eNew, proof? := p }
 
+def Result.addForalls (r : Result) (xs : Array Expr) : MetaM Result := do
+  if xs.isEmpty then return r
+  let eNew ← mkForallFVars xs r.expr
+  match r.proof? with
+  | none   => return { expr := eNew }
+  | some h =>
+    let p ← xs.foldrM (init := h) fun x h => do
+      mkForallCongr (← mkLambdaFVars #[x] h)
+    return { expr := eNew, proof? := p }
+
 end Simp
 
 export Simp (SimpM Simprocs)
diff --git a/tests/lean/run/funind_structural.lean b/tests/lean/run/funind_structural.lean
index 413a3fa296..918412a006 100644
--- a/tests/lean/run/funind_structural.lean
+++ b/tests/lean/run/funind_structural.lean
@@ -89,8 +89,8 @@ termination_by structural n
 
 /--
 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)
+  (case1 : ∀ (x : Bool) (m n : Nat) (f : Finn n), motive x m Finn.fzero f)
+  (case2 : ∀ (x : Bool) (m n : Nat) (a : Finn n), (a = Finn.fzero → False) → motive x m a 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
 -/
diff --git a/tests/lean/run/funind_unfolding.lean b/tests/lean/run/funind_unfolding.lean
new file mode 100644
index 0000000000..45aeaba6c5
--- /dev/null
+++ b/tests/lean/run/funind_unfolding.lean
@@ -0,0 +1,487 @@
+axiom testSorry : α
+
+def fib : Nat → Nat
+  | 0 => 0
+  | 1 => 1
+  | n+2 => fib n + fib (n+1)
+termination_by x => x
+
+/--
+info: fib.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : motive 0 0) (case2 : motive 1 1)
+  (case3 : ∀ (n : Nat), motive n.succ.succ (fib n + fib (n + 1))) (x✝ : Nat) : motive x✝ (fib x✝)
+-/
+#guard_msgs in
+#check fib.fun_cases_unfolding
+
+def ackermann : Nat → Nat → Nat
+  | 0, m => m + 1
+  | n+1, 0 => ackermann n 1
+  | n+1, m+1 => ackermann n (ackermann (n + 1) m)
+termination_by n m => (n, m)
+
+/--
+info: ackermann.fun_cases_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m (m + 1))
+  (case2 : ∀ (n : Nat), motive n.succ 0 (ackermann n 1))
+  (case3 : ∀ (n m : Nat), motive n.succ m.succ (ackermann n (ackermann (n + 1) m))) (x✝ x✝¹ : Nat) :
+  motive x✝ x✝¹ (ackermann x✝ x✝¹)
+-/
+#guard_msgs in
+#check ackermann.fun_cases_unfolding
+
+def fib' : Nat → Nat
+  | 0 => 0
+  | 1 => 1
+  | n => fib' (n-1) + fib' (n-2)
+decreasing_by all_goals exact testSorry
+
+/--
+info: fib'.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : motive 0 0) (case2 : motive 1 1)
+  (case3 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → motive n (fib' (n - 1) + fib' (n - 2))) (x✝ : Nat) :
+  motive x✝ (fib' x✝)
+-/
+#guard_msgs in
+#check fib'.fun_cases_unfolding
+
+def fib'' (n : Nat) : Nat :=
+  if _h : n < 2 then
+    n
+  else
+    let foo := n - 2
+    if foo < 100 then
+      fib'' (n - 1) + fib'' foo
+    else
+      0
+
+/--
+info: fib''.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), n < 2 → motive n n)
+  (case2 :
+    ∀ (n : Nat),
+      ¬n < 2 →
+        let foo := n - 2;
+        foo < 100 → motive n (fib'' (n - 1) + fib'' foo))
+  (case3 :
+    ∀ (n : Nat),
+      ¬n < 2 →
+        let foo := n - 2;
+        ¬foo < 100 → motive n 0)
+  (n : Nat) : motive n (fib'' n)
+-/
+#guard_msgs in
+#check fib''.fun_cases_unfolding
+
+-- set_option trace.Meta.FunInd true in
+def filter (p : Nat → Bool) : List Nat → List Nat
+  | [] => []
+  | x::xs => if p x then x::filter p xs else filter p xs
+
+/--
+info: filter.fun_cases (motive : (Nat → Bool) → List Nat → Prop) (case1 : ∀ (p : Nat → Bool), motive p [])
+  (case2 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), p x = true → motive p (x :: xs))
+  (case3 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), ¬p x = true → motive p (x :: xs)) (p : Nat → Bool)
+  (x✝ : List Nat) : motive p x✝
+-/
+#guard_msgs in
+#check filter.fun_cases
+
+/--
+info: filter.fun_cases_unfolding (motive : (Nat → Bool) → List Nat → List Nat → Prop)
+  (case1 : ∀ (p : Nat → Bool), motive p [] [])
+  (case2 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), p x = true → motive p (x :: xs) (x :: filter p xs))
+  (case3 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), ¬p x = true → motive p (x :: xs) (filter p xs))
+  (p : Nat → Bool) (x✝ : List Nat) : motive p x✝ (filter p x✝)
+-/
+#guard_msgs in
+#check filter.fun_cases_unfolding
+
+/--
+info: filter.induct (p : Nat → Bool) (motive : List Nat → Prop) (case1 : motive [])
+  (case2 : ∀ (x : Nat) (xs : List Nat), p x = true → motive xs → motive (x :: xs))
+  (case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive xs → motive (x :: xs)) (a✝ : List Nat) : motive a✝
+-/
+#guard_msgs in
+#check filter.induct
+
+/--
+info: filter.induct_unfolding (p : Nat → Bool) (motive : List Nat → List Nat → Prop) (case1 : motive [] [])
+  (case2 : ∀ (x : Nat) (xs : List Nat), p x = true → motive xs (filter p xs) → motive (x :: xs) (x :: filter p xs))
+  (case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive xs (filter p xs) → motive (x :: xs) (filter p xs))
+  (a✝ : List Nat) : motive a✝ (filter p a✝)
+-/
+#guard_msgs in
+#check filter.induct_unfolding
+
+theorem filter_const_false_is_nil :
+    filter (fun _ => false) xs = [] := by
+  refine filter.induct_unfolding (fun _ => false) (motive := fun xs r => r = []) ?case1 ?case2 ?case3 xs
+  case case1 => rfl
+  case case2 => intros; contradiction
+  case case3 => intros; assumption
+
+theorem filter_filter :
+    filter q (filter p xs) = filter (fun x => p x && q x) xs := by
+  refine filter.induct_unfolding p (motive := fun xs r => filter q r = filter (fun x => p x && q x) xs) ?case1 ?case2 ?case3 xs
+  case case1 => rfl
+  case case2 =>
+    intros x xs hp ih
+    by_cases hq : q x
+    case pos => simp [*, filter]
+    case neg => simp [*, filter]
+  case case3 =>
+    intros
+    simp [*, filter]
+
+
+def map (f : Nat → Bool) : List Nat → List Bool
+  | [] => []
+  | x::xs => f x::map f xs
+termination_by x => x
+
+/--
+info: map.fun_cases (motive : (Nat → Bool) → List Nat → Prop) (case1 : ∀ (f : Nat → Bool), motive f [])
+  (case2 : ∀ (f : Nat → Bool) (x : Nat) (xs : List Nat), motive f (x :: xs)) (f : Nat → Bool) (x✝ : List Nat) :
+  motive f x✝
+-/
+#guard_msgs in
+#check map.fun_cases
+
+/--
+info: map.fun_cases_unfolding (motive : (Nat → Bool) → List Nat → List Bool → Prop)
+  (case1 : ∀ (f : Nat → Bool), motive f [] [])
+  (case2 : ∀ (f : Nat → Bool) (x : Nat) (xs : List Nat), motive f (x :: xs) (f x :: map f xs)) (f : Nat → Bool)
+  (x✝ : List Nat) : motive f x✝ (map f x✝)
+-/
+#guard_msgs in
+#check map.fun_cases_unfolding
+
+/--
+info: map.induct (motive : List Nat → Prop) (case1 : motive [])
+  (case2 : ∀ (x : Nat) (xs : List Nat), motive xs → motive (x :: xs)) (a✝ : List Nat) : motive a✝
+-/
+#guard_msgs in
+#check map.induct
+
+/--
+info: map.induct_unfolding (f : Nat → Bool) (motive : List Nat → List Bool → Prop) (case1 : motive [] [])
+  (case2 : ∀ (x : Nat) (xs : List Nat), motive xs (map f xs) → motive (x :: xs) (f x :: map f xs)) (a✝ : List Nat) :
+  motive a✝ (map f a✝)
+-/
+#guard_msgs in
+#check map.induct_unfolding
+
+namespace BinaryWF
+
+def map2 (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
+  | x::xs, y::ys => f x y::map2 f xs ys
+  | _, _ => []
+termination_by x => x
+
+
+/--
+info: BinaryWF.map2.induct_unfolding (f : Nat → Nat → Bool) (motive : List Nat → List Nat → List Bool → Prop)
+  (case1 :
+    ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
+      motive xs ys (map2 f xs ys) → motive (x :: xs) (y :: ys) (f x y :: map2 f xs ys))
+  (case2 :
+    ∀ (x x_1 : List Nat),
+      (∀ (x_2 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), x = x_2 :: xs → x_1 = y :: ys → False) →
+        motive x x_1 [])
+  (a✝ a✝¹ : List Nat) : motive a✝ a✝¹ (map2 f a✝ a✝¹)
+-/
+#guard_msgs in
+#check map2.induct_unfolding
+
+end BinaryWF
+
+namespace BinaryStructural
+
+def map2 (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
+  | x::xs, y::ys => f x y::map2 f xs ys
+  | _, _ => []
+termination_by structural x => x
+
+/--
+info: BinaryStructural.map2.induct_unfolding (f : Nat → Nat → Bool) (motive : List Nat → List Nat → List Bool → Prop)
+  (case1 :
+    ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
+      motive xs ys (map2 f xs ys) → motive (x :: xs) (y :: ys) (f x y :: map2 f xs ys))
+  (case2 :
+    ∀ (t x : List Nat),
+      (∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) → motive t x [])
+  (a✝ a✝¹ : List Nat) : motive a✝ a✝¹ (map2 f a✝ a✝¹)
+-/
+#guard_msgs in
+#check map2.induct_unfolding
+
+end BinaryStructural
+
+namespace MutualWF
+
+mutual
+def map2a (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
+  | x::xs, y::ys => f x y::map2b f xs ys
+  | _, _ => []
+termination_by x => x
+def map2b (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
+  | x::xs, y::ys => f x y::map2a f xs ys
+  | _, _ => []
+termination_by x => x
+end
+
+/--
+info: MutualWF.map2a.mutual_induct_unfolding (f : Nat → Nat → Bool) (motive1 motive2 : List Nat → List Nat → List Bool → Prop)
+  (case1 :
+    ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
+      motive2 xs ys (map2b f xs ys) → motive1 (x :: xs) (y :: ys) (f x y :: map2b f xs ys))
+  (case2 :
+    ∀ (x x_1 : List Nat),
+      (∀ (x_2 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), x = x_2 :: xs → x_1 = y :: ys → False) →
+        motive1 x x_1 [])
+  (case3 :
+    ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
+      motive1 xs ys (map2a f xs ys) → motive2 (x :: xs) (y :: ys) (f x y :: map2a f xs ys))
+  (case4 :
+    ∀ (x x_1 : List Nat),
+      (∀ (x_2 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), x = x_2 :: xs → x_1 = y :: ys → False) →
+        motive2 x x_1 []) :
+  (∀ (a a_1 : List Nat), motive1 a a_1 (map2a f a a_1)) ∧ ∀ (a a_1 : List Nat), motive2 a a_1 (map2b f a a_1)
+-/
+#guard_msgs in
+#check map2a.mutual_induct_unfolding
+
+/--
+info: MutualWF.map2a.induct_unfolding (f : Nat → Nat → Bool) (motive1 motive2 : List Nat → List Nat → List Bool → Prop)
+  (case1 :
+    ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
+      motive2 xs ys (map2b f xs ys) → motive1 (x :: xs) (y :: ys) (f x y :: map2b f xs ys))
+  (case2 :
+    ∀ (x x_1 : List Nat),
+      (∀ (x_2 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), x = x_2 :: xs → x_1 = y :: ys → False) →
+        motive1 x x_1 [])
+  (case3 :
+    ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
+      motive1 xs ys (map2a f xs ys) → motive2 (x :: xs) (y :: ys) (f x y :: map2a f xs ys))
+  (case4 :
+    ∀ (x x_1 : List Nat),
+      (∀ (x_2 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), x = x_2 :: xs → x_1 = y :: ys → False) →
+        motive2 x x_1 [])
+  (a✝ a✝¹ : List Nat) : motive1 a✝ a✝¹ (map2a f a✝ a✝¹)
+-/
+#guard_msgs in
+#check map2a.induct_unfolding
+
+end MutualWF
+
+namespace MutualStructural
+
+-- set_option trace.Meta.FunInd true in
+mutual
+def map2a (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
+  | x::xs, y::ys => f x y::map2b f xs ys
+  | _, _ => []
+termination_by structural x => x
+def map2b (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
+  | x::xs, y::ys => f x y::map2a f xs ys
+  | _, _ => []
+termination_by structural x => x
+end
+
+/--
+info: MutualStructural.map2a.induct (motive_1 motive_2 : List Nat → List Nat → Prop)
+  (case1 : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), motive_2 xs ys → motive_1 (x :: xs) (y :: ys))
+  (case2 :
+    ∀ (t x : List Nat),
+      (∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) → motive_1 t x)
+  (case3 : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), motive_1 xs ys → motive_2 (x :: xs) (y :: ys))
+  (case4 :
+    ∀ (t x : List Nat),
+      (∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) → motive_2 t x)
+  (a✝ a✝¹ : List Nat) : motive_1 a✝ a✝¹
+-/
+#guard_msgs in
+#check map2a.induct
+
+
+/--
+info: MutualStructural.map2a.mutual_induct_unfolding (f : Nat → Nat → Bool)
+  (motive_1 motive_2 : List Nat → List Nat → List Bool → Prop)
+  (case1 :
+    ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
+      motive_2 xs ys (map2b f xs ys) → motive_1 (x :: xs) (y :: ys) (map2a f (x :: xs) (y :: ys)))
+  (case2 :
+    ∀ (t x : List Nat),
+      (∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) →
+        motive_1 t x (map2a f t x))
+  (case3 :
+    ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
+      motive_1 xs ys (map2a f xs ys) → motive_2 (x :: xs) (y :: ys) (map2b f (x :: xs) (y :: ys)))
+  (case4 :
+    ∀ (t x : List Nat),
+      (∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) →
+        motive_2 t x (map2b f t x)) :
+  (∀ (a a_1 : List Nat), motive_1 a a_1 (map2a f a a_1)) ∧ ∀ (a a_1 : List Nat), motive_2 a a_1 (map2b f a a_1)
+-/
+#guard_msgs in
+#check map2a.mutual_induct_unfolding
+
+
+/--
+info: MutualStructural.map2a.induct_unfolding (f : Nat → Nat → Bool)
+  (motive_1 motive_2 : List Nat → List Nat → List Bool → Prop)
+  (case1 :
+    ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
+      motive_2 xs ys (map2b f xs ys) → motive_1 (x :: xs) (y :: ys) (map2a f (x :: xs) (y :: ys)))
+  (case2 :
+    ∀ (t x : List Nat),
+      (∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) →
+        motive_1 t x (map2a f t x))
+  (case3 :
+    ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
+      motive_1 xs ys (map2a f xs ys) → motive_2 (x :: xs) (y :: ys) (map2b f (x :: xs) (y :: ys)))
+  (case4 :
+    ∀ (t x : List Nat),
+      (∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) →
+        motive_2 t x (map2b f t x))
+  (a✝ a✝¹ : List Nat) : motive_1 a✝ a✝¹ (map2a f a✝ a✝¹)
+-/
+#guard_msgs in
+#check map2a.induct_unfolding
+
+end MutualStructural
+
+
+abbrev leftChild (i : Nat) := 2*i + 1
+abbrev parent (i : Nat) := (i - 1) / 2
+
+def siftDown (a : Array Int) (root : Nat) (e : Nat) (h : e ≤ a.size := by omega) : Array Int :=
+  if _ : leftChild root < e then
+    let child := leftChild root
+    let child := if _ : child+1 < e then
+      if a[child] < a[child + 1] then
+        child + 1
+      else
+        child
+    else
+      child
+    if a[root]! < a[child]! then
+      let a := a.swapIfInBounds root child
+      siftDown a child e testSorry
+    else
+      a
+  else
+    a
+termination_by e - root
+decreasing_by exact testSorry
+
+/--
+info: siftDown.induct_unfolding (e : Nat) (motive : (a : Array Int) → Nat → e ≤ a.size → Array Int → Prop)
+  (case1 :
+    ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size),
+      leftChild root < e →
+        let child := leftChild root;
+        let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
+        a[root]! < a[child]! →
+          let a_1 := a.swapIfInBounds root child;
+          motive a_1 child ⋯ (siftDown a_1 child e ⋯) → motive a root h (siftDown a_1 child e ⋯))
+  (case2 :
+    ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size),
+      leftChild root < e →
+        let child := leftChild root;
+        let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
+        ¬a[root]! < a[child]! → motive a root h a)
+  (case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h a) (a : Array Int)
+  (root : Nat) (h : e ≤ a.size) : motive a root h (siftDown a root e h)
+-/
+#guard_msgs in
+#check siftDown.induct_unfolding
+
+/--
+info: siftDown.induct (e : Nat) (motive : (a : Array Int) → Nat → e ≤ a.size → Prop)
+  (case1 :
+    ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size),
+      leftChild root < e →
+        let child := leftChild root;
+        let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
+        a[root]! < a[child]! →
+          let a_1 := a.swapIfInBounds root child;
+          motive a_1 child ⋯ → motive a root h)
+  (case2 :
+    ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size),
+      leftChild root < e →
+        let child := leftChild root;
+        let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
+        ¬a[root]! < a[child]! → motive a root h)
+  (case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h) (a : Array Int)
+  (root : Nat) (h : e ≤ a.size) : motive a root h
+-/
+#guard_msgs in
+#check siftDown.induct
+
+-- Now something with have
+
+def withHave (n : Nat): Bool :=
+  have : 0 < n := testSorry
+  if n = 42 then true else withHave (n - 1)
+termination_by n
+decreasing_by exact testSorry
+
+/--
+info: withHave.induct_unfolding (motive : Nat → Bool → Prop) (case1 : 0 < 42 → motive 42 true)
+  (case2 : ∀ (x : Nat), 0 < x → ¬x = 42 → motive (x - 1) (withHave (x - 1)) → motive x (withHave (x - 1))) (n : Nat) :
+  motive n (withHave n)
+-/
+#guard_msgs in
+#check withHave.induct_unfolding
+
+/--
+info: withHave.fun_cases_unfolding (motive : Nat → Bool → Prop) (case1 : 0 < 42 → motive 42 true)
+  (case2 : ∀ (n : Nat), 0 < n → ¬n = 42 → motive n (withHave (n - 1))) (n : Nat) : motive n (withHave n)
+-/
+#guard_msgs in
+#check withHave.fun_cases_unfolding
+
+-- Structural Mutual recursion
+
+inductive Tree (α : Type u) : Type u where
+  | node : α → (Bool → List (Tree α)) → Tree α
+
+mutual
+def Tree.size : Tree α → Nat
+  | .node _ tsf => 1 + size_aux (tsf true) + size_aux (tsf false)
+termination_by structural t => t
+def Tree.size_aux : List (Tree α) → Nat
+  | [] => 0
+  | t :: ts => size t + size_aux ts
+end
+
+/--
+info: Tree.size.induct_unfolding.{u_1} {α : Type u_1} (motive_1 : Tree α → Nat → Prop) (motive_2 : List (Tree α) → Nat → Prop)
+  (case1 :
+    ∀ (a : α) (tsf : Bool → List (Tree α)),
+      motive_2 (tsf true) (Tree.size_aux (tsf true)) →
+        motive_2 (tsf false) (Tree.size_aux (tsf false)) →
+          motive_1 (Tree.node a tsf) (1 + Tree.size_aux (tsf true) + Tree.size_aux (tsf false)))
+  (case2 : motive_2 [] 0)
+  (case3 :
+    ∀ (t : Tree α) (ts : List (Tree α)),
+      motive_1 t t.size → motive_2 ts (Tree.size_aux ts) → motive_2 (t :: ts) (t.size + Tree.size_aux ts))
+  (a✝ : Tree α) : motive_1 a✝ a✝.size
+-/
+#guard_msgs in
+#check Tree.size.induct_unfolding
+
+/--
+info: Tree.size_aux.induct_unfolding.{u_1} {α : Type u_1} (motive_1 : Tree α → Nat → Prop)
+  (motive_2 : List (Tree α) → Nat → Prop)
+  (case1 :
+    ∀ (a : α) (tsf : Bool → List (Tree α)),
+      motive_2 (tsf true) (Tree.size_aux (tsf true)) →
+        motive_2 (tsf false) (Tree.size_aux (tsf false)) →
+          motive_1 (Tree.node a tsf) (1 + Tree.size_aux (tsf true) + Tree.size_aux (tsf false)))
+  (case2 : motive_2 [] 0)
+  (case3 :
+    ∀ (t : Tree α) (ts : List (Tree α)),
+      motive_1 t t.size → motive_2 ts (Tree.size_aux ts) → motive_2 (t :: ts) (t.size + Tree.size_aux ts))
+  (a✝ : List (Tree α)) : motive_2 a✝ (Tree.size_aux a✝)
+-/
+#guard_msgs in
+#check Tree.size_aux.induct_unfolding
diff --git a/tests/lean/run/funinduction_generalize.lean b/tests/lean/run/funinduction_generalize.lean
index d34db2c470..ca9dd936c4 100644
--- a/tests/lean/run/funinduction_generalize.lean
+++ b/tests/lean/run/funinduction_generalize.lean
@@ -27,9 +27,9 @@ ih1✝ : P (xs✝.zip ys✝)
 case case2
 xs ys : List Nat
 P : {α : Type} → List α → Prop
-t✝ x✝¹ : List Nat
-x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
-⊢ P (t✝.zip x✝¹)
+t✝ ys✝ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
+⊢ P (t✝.zip ys✝)
 -/
 #guard_msgs in
 example : P (List.zip xs ys) := by
@@ -52,10 +52,10 @@ h : (x✝ :: xs✝).isEmpty = true
 case case2
 xs ys : List Nat
 P : {α : Type} → List α → Prop
-t✝ x✝¹ : List Nat
-x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+t✝ ys✝ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
 h : t✝.isEmpty = true
-⊢ P (t✝.zip x✝¹)
+⊢ P (t✝.zip ys✝)
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
@@ -78,8 +78,8 @@ h : (x✝ :: xs✝).isEmpty = true
 case case2
 xs ys : List Nat
 P : {α : Type} → List α → Prop
-t✝ x✝¹ : List Nat
-x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+t✝ ys✝ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
 h : t✝.isEmpty = true
 ⊢ P (t✝.zip ys)
 -/
@@ -103,8 +103,8 @@ h : (x✝ :: xs✝).isEmpty = true
 case case2
 xs ys : List Nat
 P : {α : Type} → List α → Prop
-t✝ x✝¹ : List Nat
-x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+t✝ ys✝ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
 h : t✝.isEmpty = true
 ⊢ P (t✝.zip ys)
 -/
@@ -129,9 +129,9 @@ case case2
 xs ys : List Nat
 P : {α : Type} → List α → Prop
 h : xs.isEmpty = true
-t✝ x✝¹ : List Nat
-x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
-⊢ P (xs.zip x✝¹)
+t✝ ys✝ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
+⊢ P (xs.zip ys✝)
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
@@ -154,9 +154,9 @@ case case2
 xs ys : List Nat
 P : {α : Type} → List α → Prop
 h : xs.isEmpty = true
-t✝ x✝¹ : List Nat
-x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
-⊢ P (xs.zip x✝¹)
+t✝ ys✝ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
+⊢ P (xs.zip ys✝)
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
@@ -177,11 +177,11 @@ h : xs.isEmpty = true
 
 case case2
 P : {α : Type} → List α → Prop
-t✝ x✝¹ : List Nat
-x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+t✝ ys✝ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
 xs : List Nat
 h : xs.isEmpty = true
-⊢ P (xs.zip x✝¹)
+⊢ P (xs.zip ys✝)
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
@@ -202,11 +202,11 @@ h : xs.isEmpty = true
 
 case case2
 P : {α : Type} → List α → Prop
-t✝ x✝¹ : List Nat
-x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+t✝ ys✝ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
 xs : List Nat
 h : xs.isEmpty = true
-⊢ P (xs.zip x✝¹)
+⊢ P (xs.zip ys✝)
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by