diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index bf0de8759e..805044fcb8 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -228,14 +228,27 @@ def withAnnotateTermInfo (d : Delab) : Delab := do
   let stx ← d
   annotateTermInfo stx
 
-def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do
-  -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
-  let suggestion := if suggestion.isAnonymous then `a else suggestion
-  -- We use this small hack to convert identifiers created using `mkAuxFunDiscr` to simple names
-  let suggestion := suggestion.eraseMacroScopes
+/--
+Gets an name based on `suggestion` that is unused in the local context.
+Erases macro scopes.
+If `pp.safeShadowing` is true, then the name is allowed to shadow a name in the local context
+if the name does not appear in `body`.
+
+If `preserveName` is false, then returns the name, possibly with fresh macro scopes added.
+If `suggestion` has macro scopes then the result does as well.
+-/
+def getUnusedName (suggestion : Name) (body : Expr) (preserveName : Bool := false) : DelabM Name := do
+  let (hasScopes, suggestion) :=
+    if suggestion.isAnonymous then
+      -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
+      (true, `a)
+    else
+      (suggestion.hasMacroScopes, suggestion.eraseMacroScopes)
   let lctx ← getLCtx
-  if !lctx.usesUserName suggestion then
+  if !lctx.usesUserName suggestion || (preserveName && !hasScopes) then
     return suggestion
+  else if preserveName then
+    withFreshMacroScope <| MonadQuotation.addMacroScope suggestion
   else if (← getPPOption getPPSafeShadowing) && !bodyUsesSuggestion lctx suggestion then
     return suggestion
   else
@@ -262,9 +275,12 @@ def mkAnnotatedIdent (n : Name) (e : Expr) : DelabM Ident := do
 Enters the body of the current expression, which must be a lambda or forall.
 The binding variable is passed to `d` as `Syntax`, and it is an identifier that has been annotated with the fvar expression
 for the variable.
+
+If `preserveName` is `false` (the default), gives the binder an unused name.
+Otherwise, it tries to preserve the textual form of the name, preserving whether it is hygienic.
 -/
-def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
-  let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody!
+def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) (preserveName := false) : DelabM α := do
+  let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody! (preserveName := preserveName)
   withBindingBody' n (mkAnnotatedIdent n) (d ·)
 
 inductive OmissionReason
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 17e0d219e5..138bde803b 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -887,24 +887,31 @@ def delabLam : Delab :=
       else
         `(fun $binders* => $stxBody)
 
+/-- Don't do any renaming for forall binders, but do add fresh macro scopes when there is shadowing. -/
+private def ppPiPreserveNames := `pp.piPreserveNames
+/-- Causes non-dependent foralls to print with binder names. -/
+private def ppPiBinderNames := `pp.piBinderNames
+
 /--
 Similar to `delabBinders`, but tracking whether `forallE` is dependent or not.
 
 See issue #1571
 -/
 private partial def delabForallBinders (delabGroup : Array Syntax → Bool → Syntax → Delab) (curNames : Array Syntax := #[]) (curDep := false) : Delab := do
-  let dep := !(← getExpr).isArrow
+  -- Logic note: wanting to print with binder names is equivalent to pretending the forall is dependent.
+  let dep := !(← getExpr).isArrow || (← getOptionsAtCurrPos).get ppPiBinderNames false
   if !curNames.isEmpty && dep != curDep then
     -- don't group
     delabGroup curNames curDep (← delab)
   else
+    let preserve := (← getOptionsAtCurrPos).get ppPiPreserveNames false
     let curDep := dep
     if ← shouldGroupWithNext then
       -- group with nested binder => recurse immediately
-      withBindingBodyUnusedName fun stxN => delabForallBinders delabGroup (curNames.push stxN) curDep
+      withBindingBodyUnusedName (preserveName := preserve) fun stxN => delabForallBinders delabGroup (curNames.push stxN) curDep
     else
       -- don't group => delab body and prepend current binder group
-      let (stx, stxN) ← withBindingBodyUnusedName fun stxN => return (← delab, stxN)
+      let (stx, stxN) ← withBindingBodyUnusedName (preserveName := preserve) fun stxN => return (← delab, stxN)
       delabGroup (curNames.push stxN) curDep stx
 
 @[builtin_delab forallE]
@@ -1297,11 +1304,13 @@ where
       -- but this would be the usual case.
       let group ← withBindingDomain do `(bracketedBinderF|[$(← delabTy)])
       withBindingBody e.bindingName! <| delabParams bindingNames idStx (groups.push group)
-    else if e.isForall && !e.bindingName!.hasMacroScopes && !bindingNames.contains e.bindingName! then
+    else if e.isForall && (!e.isArrow || !(e.bindingName!.hasMacroScopes || bindingNames.contains e.bindingName!)) then
       delabParamsAux bindingNames idStx groups #[]
     else
-      let type ← delabTy
-      `(declSigWithId| $idStx:ident $groups* : $type)
+      let (opts', e') ← processSpine {} (← readThe SubExpr)
+      withReader (fun ctx => {ctx with optionsPerPos := opts', subExpr := { ctx.subExpr with expr := e' }}) do
+        let type ← delabTy
+        `(declSigWithId| $idStx:ident $groups* : $type)
   /--
   Inner loop for `delabParams`, collecting binders.
   Invariants:
@@ -1311,6 +1320,7 @@ where
   -/
   delabParamsAux (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
     let e@(.forallE n d e' i) ← getExpr | unreachable!
+    let n ← if bindingNames.contains n then withFreshMacroScope <| MonadQuotation.addMacroScope n else pure n
     let bindingNames := bindingNames.insert n
     let stxN := mkIdent n
     let curIds := curIds.push ⟨stxN⟩
@@ -1336,13 +1346,34 @@ where
   -/
   shouldGroupWithNext (bindingNames : NameSet) (e e' : Expr) : Bool :=
     e'.isForall &&
-    -- At the first sign of an inaccessible name, stop merging binders:
-    !e'.bindingName!.hasMacroScopes &&
-    -- If it's a name that has already been used, stop merging binders:
-    !bindingNames.contains e'.bindingName! &&
+    (!e'.isArrow ||
+      -- At the first sign of an inaccessible name, stop merging binders:
+    !(e'.bindingName!.hasMacroScopes ||
+      -- If it's a name that has already been used, stop merging binders:
+      bindingNames.contains e'.bindingName!)) &&
     e.binderInfo == e'.binderInfo &&
     e.bindingDomain! == e'.bindingDomain! &&
     -- Inst implicits can't be grouped:
     e'.binderInfo != BinderInfo.instImplicit
+  /--
+  Go through rest of type, alpha renaming and setting options along the spine.
+  -/
+  processSpine (opts : OptionsPerPos) (subExpr : SubExpr) : MetaM (OptionsPerPos × Expr) := do
+    if let .forallE n t b bi := subExpr.expr then
+      let used := (← getLCtx).usesUserName n
+      withLocalDecl n bi t fun fvar => do
+        let (opts, b') ← processSpine opts { expr := b.instantiate1 fvar, pos := subExpr.pos.pushBindingBody }
+        let b' := b'.abstract #[fvar]
+        let opts := opts.insertAt subExpr.pos ppPiPreserveNames true
+        if n.hasMacroScopes then
+          return (opts, .forallE n t b' bi)
+        else if !used then
+          let opts := opts.insertAt subExpr.pos ppPiBinderNames true
+          return (opts, .forallE n t b' bi)
+        else
+          let n' ← withFreshMacroScope <| MonadQuotation.addMacroScope n
+          return (opts, .forallE n' t b' bi)
+    else
+      return (opts, subExpr.expr)
 
 end Lean.PrettyPrinter.Delaborator
diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
index dfa8311f3e..30909660e4 100644
--- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
@@ -18,6 +18,14 @@ namespace Lean.PrettyPrinter.Delaborator
 
 abbrev OptionsPerPos := RBMap SubExpr.Pos Options compare
 
+def OptionsPerPos.insertAt (optionsPerPos : OptionsPerPos) (pos : SubExpr.Pos) (name : Name) (value : DataValue) : OptionsPerPos :=
+  let opts := optionsPerPos.find? pos |>.getD {}
+  optionsPerPos.insert pos <| opts.insert name value
+
+/-- Merges two collections of options, where the second overrides the first. -/
+def OptionsPerPos.merge : OptionsPerPos → OptionsPerPos → OptionsPerPos :=
+  RBMap.mergeBy (fun _ => KVMap.mergeBy (fun _ _ dv => dv))
+
 namespace SubExpr
 
 open Lean.SubExpr
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 8b9324fe3d..23f7ec3042 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -30,16 +30,18 @@ structure Context where
 
 structure State where
   stxTrav  : Syntax.Traverser
-  -- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual
-  -- content of `stack` is modified only by `pushText` and `pushLine`, so `leadWord` is adjusted there accordingly.
+  /-- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual
+  content of `stack` is modified only by `pushText` and `pushLine`, so `leadWord` is adjusted there accordingly. -/
   leadWord : String := ""
-  -- Whether the generated format begins with the result of an ungrouped category formatter.
+  /-- When the `leadWord` is nonempty, whether it is an identifier. Identifiers get space inserted between them. -/
+  leadWordIdent : Bool := false
+  /-- Whether the generated format begins with the result of an ungrouped category formatter. -/
   isUngrouped : Bool := false
-  -- Whether the resulting format must be grouped when used in a category formatter.
-  -- If the flag is set to false, then categoryParser omits the fill+nest operation.
+  /-- Whether the resulting format must be grouped when used in a category formatter.
+  If the flag is set to false, then categoryParser omits the fill+nest operation. -/
   mustBeGrouped : Bool := true
-  -- Stack of generated Format objects, analogous to the Syntax stack in the parser.
-  -- Note, however, that the stack is reversed because of the right-to-left traversal.
+  /-- Stack of generated Format objects, analogous to the Syntax stack in the parser.
+  Note, however, that the stack is reversed because of the right-to-left traversal. -/
   stack    : Array Format := #[]
 
 end Formatter
@@ -121,7 +123,7 @@ private def push (f : Format) : FormatterM Unit :=
 
 def pushWhitespace (f : Format) : FormatterM Unit := do
   push f
-  modify fun st => { st with leadWord := "", isUngrouped := false }
+  modify fun st => { st with leadWord := "", leadWordIdent := false, isUngrouped := false }
 
 def pushLine : FormatterM Unit :=
   pushWhitespace Format.line
@@ -335,7 +337,7 @@ def parseToken (s : String) : FormatterM ParserState :=
     options := ← getOptions
   } ((← read).table) (Parser.mkParserState s)
 
-def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
+def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit := do
   match info with
   | SourceInfo.original _ _ ss _ =>
     -- preserve non-whitespace content (i.e. comments)
@@ -346,23 +348,34 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
         push s!"\n{ss'}"
       else
         push s!"  {ss'}"
-      modify fun st => { st with leadWord := "" }
+      modify fun st => { st with leadWord := "", leadWordIdent := false }
   | _ => pure ()
 
   let st ← get
-  -- If there is no space between `tk` and the next word, see if we would parse more than `tk` as a single token
+  -- If there is no space between `tk` and the next word, see if we should insert a discretionary space.
   if st.leadWord != "" && tk.trimRight == tk then
-    let tk' := tk.trimLeft
-    let t ← parseToken $ tk' ++ st.leadWord
-    if t.pos <= tk'.endPos then
-      -- stopped within `tk` => use it as is, extend `leadWord` if not prefixed by whitespace
+    let insertSpace ← do
+      if ident && st.leadWordIdent then
+        -- Both idents => need space
+        pure true
+      else
+        -- Check if we would parse more than `tk` as a single token
+        let tk' := tk.trimLeft
+        let t ← parseToken $ tk' ++ st.leadWord
+        if t.pos ≤ tk'.endPos then
+          -- stopped within `tk` => use it as is
+          pure false
+        else
+          -- stopped after `tk` => add space
+          pure true
+    if !insertSpace then
+      -- extend `leadWord` if not prefixed by whitespace
       push tk
-      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "" }
+      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "", leadWordIdent := ident }
     else
-      -- stopped after `tk` => add space
       pushLine
       push tk
-      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
+      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "", leadWordIdent := ident }
   else
     -- already separated => use `tk` as is
     if st.leadWord == "" then
@@ -372,7 +385,7 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
       push tk.trimRight
     else
       push tk -- preserve special whitespace for tokens like ":=\n"
-    modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
+    modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "", leadWordIdent := ident }
 
   match info with
   | SourceInfo.original ss _ _ _ =>
@@ -395,7 +408,7 @@ def symbolNoAntiquot.formatter (sym : String) : Formatter := do
   let stx ← getCur
   if stx.isToken sym then do
     let (Syntax.atom info _) ← pure stx | unreachable!
-    withMaybeTag (getExprPos? stx) (pushToken info sym)
+    withMaybeTag (getExprPos? stx) (pushToken info sym false)
     goLeft
   else do
     trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected symbol '{sym}'"
@@ -410,9 +423,9 @@ def unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter := do
   let Syntax.atom info val ← getCur
     | throwError m!"not an atom: {← getCur}"
   if val == sym.trim then
-    pushToken info sym
+    pushToken info sym false
   else
-    pushToken info asciiSym;
+    pushToken info asciiSym false
   goLeft
 
 @[combinator_formatter identNoAntiquot]
@@ -423,14 +436,14 @@ def identNoAntiquot.formatter : Formatter := do
   let id := id.simpMacroScopes
   let table := (← read).table
   let isToken (s : String) : Bool := (table.find? s).isSome
-  withMaybeTag (getExprPos? stx) (pushToken info (id.toString (isToken := isToken)))
+  withMaybeTag (getExprPos? stx) (pushToken info (id.toString (isToken := isToken)) true)
   goLeft
 
 @[combinator_formatter rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do
   checkKind identKind
   let Syntax.ident info _ id _ ← getCur
     | throwError m!"not an ident: {← getCur}"
-  pushToken info id.toString
+  pushToken info id.toString true
   goLeft
 
 @[combinator_formatter identEq] def identEq.formatter (_id : Name) := rawIdentNoAntiquot.formatter
@@ -441,7 +454,7 @@ def visitAtom (k : SyntaxNodeKind) : Formatter := do
     checkKind k
   let Syntax.atom info val ← pure $ stx.ifNode (fun n => n.getArg 0) (fun _ => stx)
     | throwError m!"not an atom: {stx}"
-  pushToken info val
+  pushToken info val false
   goLeft
 
 @[combinator_formatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind
@@ -490,7 +503,7 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
 @[combinator_formatter checkStackTop] def checkStackTop.formatter : Formatter := pure ()
 @[combinator_formatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter :=
   -- prevent automatic whitespace insertion
-  modify fun st => { st with leadWord := "" }
+  modify fun st => { st with leadWord := "", leadWordIdent := false }
 @[combinator_formatter checkLinebreakBefore] def checkLinebreakBefore.formatter : Formatter := pure ()
 @[combinator_formatter checkTailWs] def checkTailWs.formatter : Formatter := pure ()
 @[combinator_formatter checkColEq] def checkColEq.formatter : Formatter := pure ()
diff --git a/src/lake/Lake/Toml/ParserUtil.lean b/src/lake/Lake/Toml/ParserUtil.lean
index 43e3d2070e..de874dc035 100644
--- a/src/lake/Lake/Toml/ParserUtil.lean
+++ b/src/lake/Lake/Toml/ParserUtil.lean
@@ -161,7 +161,7 @@ open Formatter Syntax.MonadTraverser in
   let .atom info val := stx
     | trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected atom"
       throwBacktrack
-  withMaybeTag (getSyntaxExprPos? stx) (pushToken info val)
+  withMaybeTag (getSyntaxExprPos? stx) (pushToken info val false)
   goLeft
 
 @[combinator_parenthesizer atom]
diff --git a/tests/lean/autoImplicitChainNameIssue.lean.expected.out b/tests/lean/autoImplicitChainNameIssue.lean.expected.out
index 749246019c..a56d97e58d 100644
--- a/tests/lean/autoImplicitChainNameIssue.lean.expected.out
+++ b/tests/lean/autoImplicitChainNameIssue.lean.expected.out
@@ -3,4 +3,4 @@ case nil
 α✝ : Type u_1
 as : List α✝
 ⊢ Palindrome [].reverse
-palindrome_reverse.{u_1} : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome as.reverse
+palindrome_reverse.{u_1} {α✝ : Type u_1} {as : List α✝} (h : Palindrome as) : Palindrome as.reverse
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index 14f9bcfa50..c5afb1731d 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -46,6 +46,6 @@ fun x =>
   | #[] => 0
   | #[3, 4, 5] => 3
   | x => 4 : Array Nat → Nat
-g.match_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) :
-  (x : List α) → ((a : α) → motive [a]) → ((x : List α) → motive x) → motive x
+g.match_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α) (h_1 : (a : α) → motive [a])
+  (h_2 : (x : List α) → motive x) : motive x✝
 fun e => nomatch e : Empty → False
diff --git a/tests/lean/run/2846.lean b/tests/lean/run/2846.lean
index 88dcf2f153..5bd6aab0f8 100644
--- a/tests/lean/run/2846.lean
+++ b/tests/lean/run/2846.lean
@@ -30,31 +30,41 @@ def Nat.pos_pow_of_pos' {n : Nat} (m : Nat) : 0 < n → 0 < n ^ m := Nat.pos_pow
 
 /-!
 Repetition of a named argument, only the first is printed as a named argument.
+The second is made hygienic.
 -/
 def foo (n n : Nat) : Fin (n + 1) := 0
 
-/-- info: foo (n : Nat) : (n : Nat) → Fin (n + 1) -/
+/-- info: foo (n n✝ : Nat) : Fin (n✝ + 1) -/
 #guard_msgs in #check foo
 
 /-!
-Repetition of a named argument, only the first is printed as a named argument.
-This is checking that shadowing is handled correctly (that's not the responsibility of
-`delabConstWithSignature`, but it assumes that the main delaborator will handle this correctly).
+Same, but a named argument still follows, and its name is preserved.
 -/
+
 def foo' (n n : Nat) (a : Fin ((by clear n; exact n) + 1)) : Fin (n + 1) := 0
 
-/-- info: foo' (n : Nat) : (n_1 : Nat) → Fin (n + 1) → Fin (n_1 + 1) -/
+/-- info: foo' (n n✝ : Nat) (a : Fin (n + 1)) : Fin (n✝ + 1) -/
 #guard_msgs in #check foo'
 
 /-!
-Named argument after inaccessible name, still stays after the colon.
-But, it does not print using named pi notation since this is not a dependent type.
+Named argument after non-dependent inaccessible name, still stays after the colon.
+Prints with named pi notation.
 -/
 def foo'' : String → (needle : String) → String := fun _ yo => yo
 
-/-- info: foo'' : String → String → String -/
+/-- info: foo'' : String → (needle : String) → String -/
 #guard_msgs in #check foo''
 
+/-!
+Named argument after inaccessible name that's still a dependent argument.
+Stays before the colon, and the names are grouped.
+-/
+
+def foo''' : (_ : Nat) → (n : Nat) → Fin (n + by clear n; assumption) := sorry
+
+/-- info: foo''' (x✝ n : Nat) : Fin (n + x✝) -/
+#guard_msgs in #check foo'''
+
 /-!
 Named argument after inaccessible name, still stays after the colon.
 Here, because it's a dependent type the named pi notation shows the name.
diff --git a/tests/lean/run/4320.lean b/tests/lean/run/4320.lean
index b524a9fb0b..adcdfd4a3d 100644
--- a/tests/lean/run/4320.lean
+++ b/tests/lean/run/4320.lean
@@ -8,7 +8,7 @@ def many_map {α β : Type} (f : α → β) : Many α → Many β
 
 /--
 info: many_map.induct {α β : Type} (f : α → β) (motive : Many α → Prop) (case1 : motive Many.none)
-  (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) : ∀ (a : Many α), motive a
+  (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) (a✝ : Many α) : motive a✝
 -/
 #guard_msgs in
 #check many_map.induct
diff --git a/tests/lean/run/5424.lean b/tests/lean/run/5424.lean
index 92a64df01b..cf38cb7833 100644
--- a/tests/lean/run/5424.lean
+++ b/tests/lean/run/5424.lean
@@ -1,3 +1,4 @@
+import Lean
 /-!
 # Long runs of identifiers should include line breaks
 -/
@@ -19,3 +20,12 @@ info: foo
   Nat
 -/
 #guard_msgs(whitespace := exact) in #check foo
+
+/-!
+Issue pointed out by Mario: need spaces between `x✝` and `y✝`.
+-/
+/--
+info: def foo✝ (x✝ y✝ : Nat✝) :=
+  x✝
+-/
+#guard_msgs in #eval do Lean.PrettyPrinter.ppCommand (← `(command| def foo (x y : Nat) := x))
diff --git a/tests/lean/run/974.lean b/tests/lean/run/974.lean
index 395d1918c2..a27878533e 100644
--- a/tests/lean/run/974.lean
+++ b/tests/lean/run/974.lean
@@ -11,24 +11,23 @@ def Formula.count_quantifiers : {n:Nat} → Formula n → Nat
 attribute [simp] Formula.count_quantifiers
 
 /--
-info: Formula.count_quantifiers.eq_1.{u_1} :
-  ∀ (x : Nat) (f₁ f₂ : Formula x), (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers
+info: Formula.count_quantifiers.eq_1.{u_1} (x✝ : Nat) (f₁ f₂ : Formula x✝) :
+  (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_1
 
 /--
-info: Formula.count_quantifiers.eq_2.{u_1} :
-  ∀ (x : Nat) (f : Formula (x + 1)), f.all.count_quantifiers = f.count_quantifiers + 1
+info: Formula.count_quantifiers.eq_2.{u_1} (x✝ : Nat) (f : Formula (x✝ + 1)) :
+  f.all.count_quantifiers = f.count_quantifiers + 1
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_2
 
 /--
-info: Formula.count_quantifiers.eq_3.{u_1} :
-  ∀ (x : Nat) (x_1 : Formula x),
-    (∀ (f₁ f₂ : Formula x), x_1 = f₁.imp f₂ → False) →
-      (∀ (f : Formula (x + 1)), x_1 = f.all → False) → x_1.count_quantifiers = 0
+info: Formula.count_quantifiers.eq_3.{u_1} (x✝ : Nat) (x✝¹ : Formula x✝)
+  (x_4 : ∀ (f₁ f₂ : Formula x✝), x✝¹ = f₁.imp f₂ → False) (x_5 : ∀ (f : Formula (x✝ + 1)), x✝¹ = f.all → False) :
+  x✝¹.count_quantifiers = 0
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_3
diff --git a/tests/lean/run/eqnsPrio.lean b/tests/lean/run/eqnsPrio.lean
index 97613ad6e8..1d33ae6bb9 100644
--- a/tests/lean/run/eqnsPrio.lean
+++ b/tests/lean/run/eqnsPrio.lean
@@ -11,13 +11,13 @@ def foo : Bool → Nat → Nat
   | _, n+1 => foo .false n
 termination_by _ n => n
 
-/-- info: foo.eq_1 : ∀ (x : Bool), foo x 0 = 0 -/
+/-- info: foo.eq_1 (x✝ : Bool) : foo x✝ 0 = 0 -/
 #guard_msgs in
 #check foo.eq_1
 /-- info: foo.eq_2 (n : Nat) : foo true n.succ = foo true n -/
 #guard_msgs in
 #check foo.eq_2
-/-- info: foo.eq_3 : ∀ (x : Bool) (n : Nat), (x = true → False) → foo x n.succ = foo false n -/
+/-- info: foo.eq_3 (x✝ : Bool) (n : Nat) (x_3 : x✝ = true → False) : foo x✝ n.succ = foo false n -/
 #guard_msgs in
 #check foo.eq_3
 
diff --git a/tests/lean/run/funind_demo.lean b/tests/lean/run/funind_demo.lean
index f27d0d4808..deca8f44c6 100644
--- a/tests/lean/run/funind_demo.lean
+++ b/tests/lean/run/funind_demo.lean
@@ -8,8 +8,8 @@ def ackermann : Nat → Nat → Nat
 /--
 info: 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) :
-  ∀ (a a_1 : Nat), motive a a_1
+  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) (a✝ a✝¹ : Nat) :
+  motive a✝ a✝¹
 -/
 #guard_msgs in
 #check ackermann.induct
@@ -19,7 +19,7 @@ def Tree.rev : Tree → Tree | node ts => .node (ts.attach.map (fun ⟨t, _ht⟩
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
-  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a
+  (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_fewer_levels.lean b/tests/lean/run/funind_fewer_levels.lean
index 519b4e44bf..453021165d 100644
--- a/tests/lean/run/funind_fewer_levels.lean
+++ b/tests/lean/run/funind_fewer_levels.lean
@@ -10,8 +10,8 @@ def foo.{u} : Nat → PUnit.{u}
 | n+1 => foo n
 
 /--
-info: Structural.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+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
@@ -31,7 +31,7 @@ termination_by xs => xs
 
 /--
 info: WellFounded.foo.induct.{v} {α : Type v} (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) : ∀ (a : List α), motive a
+  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -58,7 +58,7 @@ end
 
 /--
 info: Mutual.foo.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
-  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a : Nat), motive1 a
+  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (a✝ : Nat) : motive1 a✝
 -/
 #guard_msgs in
 #check foo.induct
diff --git a/tests/lean/run/funind_proof.lean b/tests/lean/run/funind_proof.lean
index bff44bf0e4..f6b24b0c02 100644
--- a/tests/lean/run/funind_proof.lean
+++ b/tests/lean/run/funind_proof.lean
@@ -35,7 +35,7 @@ info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2
   (case1 : ∀ (a_1 : String), (a == a_1) = true → motive1 (const a_1))
   (case2 : ∀ (a_1 : String), ¬(a == a_1) = true → motive1 (const a_1))
   (case3 : ∀ (a : String) (cs : List Term), motive2 cs → motive1 (app a cs)) (case4 : motive2 [])
-  (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) : ∀ (a : Term), motive1 a
+  (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) (a✝ : Term) : motive1 a✝
 -/
 #guard_msgs in
 #check replaceConst.induct
diff --git a/tests/lean/run/funind_structural.lean b/tests/lean/run/funind_structural.lean
index 20b6ce5f56..16b9597626 100644
--- a/tests/lean/run/funind_structural.lean
+++ b/tests/lean/run/funind_structural.lean
@@ -11,7 +11,7 @@ termination_by structural x => x
 
 /--
 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
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check fib.induct
@@ -24,8 +24,8 @@ termination_by structural x => x
 
 /--
 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
+  (case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc)
+  (a✝ a✝¹ : Nat) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check binary.induct
@@ -40,8 +40,8 @@ termination_by structural _ x => x
 /--
 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
+  (case3 : ∀ (acc : Bool) (n : Nat), motive acc (n + 1) → motive (binary' acc (n + 1)) n → motive acc n.succ.succ)
+  (a✝ : Bool) (a✝¹ : Nat) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check binary'.induct
@@ -55,8 +55,8 @@ termination_by structural x => x
 /--
 info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
   (case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (t : List α), (t = [] → False) → motive t [])
-  (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) :
-  ∀ (a : List α) (a_1 : List β), motive a a_1
+  (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) (a✝ : List α)
+  (a✝¹ : List β) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check zip.induct
@@ -94,7 +94,7 @@ info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n
   (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
+  {n : Nat} (m : Nat) (a✝ f : Finn n) : motive x m a✝ f
 -/
 #guard_msgs in
 #check Finn.min.induct
@@ -195,7 +195,7 @@ info: TermDenote.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} →
   (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
+  {ctx : List Ty} {ty : Ty} (a✝ : Term ctx ty) (a✝¹ : HList Ty.denote ctx) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check TermDenote.Term.denote.induct
diff --git a/tests/lean/run/funind_structural_mutual.lean b/tests/lean/run/funind_structural_mutual.lean
index 399764103c..8f5825658b 100644
--- a/tests/lean/run/funind_structural_mutual.lean
+++ b/tests/lean/run/funind_structural_mutual.lean
@@ -25,8 +25,8 @@ end
 info: Tree.size.induct.{u_1} {α : Type u_1} (motive_1 : Tree α → Prop) (motive_2 : List (Tree α) → Prop)
   (case1 :
     ∀ (a : α) (tsf : Bool → List (Tree α)), motive_2 (tsf true) → motive_2 (tsf false) → motive_1 (Tree.node a tsf))
-  (case2 : motive_2 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_1 t → motive_2 ts → motive_2 (t :: ts)) :
-  ∀ (a : Tree α), motive_1 a
+  (case2 : motive_2 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_1 t → motive_2 ts → motive_2 (t :: ts))
+  (a✝ : Tree α) : motive_1 a✝
 -/
 #guard_msgs in
 #check Tree.size.induct
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 503052b211..d33297ab6b 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -15,8 +15,8 @@ termination_by p => p
 /--
 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)) :
-  ∀ (a : Nat × Nat), motive a
+  (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
@@ -34,8 +34,8 @@ termination_by n m => (n, m)
 /--
 info: Binary.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) :
-  ∀ (a a_1 : Nat), motive a a_1
+  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) (a✝ a✝¹ : Nat) :
+  motive a✝ a✝¹
 -/
 #guard_msgs in
 #check ackermann.induct
@@ -50,7 +50,7 @@ def Tree.rev : Tree → Tree
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
-  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a
+  (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
 
 /--
 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
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check fib.induct
@@ -78,8 +78,8 @@ def have_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-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
+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
@@ -94,8 +94,8 @@ def have_non_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+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
@@ -109,8 +109,8 @@ def let_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+info: let_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_tailrec.induct
@@ -125,8 +125,8 @@ def let_non_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+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
@@ -145,7 +145,7 @@ termination_by n => n
 /--
 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) : ∀ (a : Nat), motive a
+  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check with_ite_tailrec.induct
@@ -165,7 +165,7 @@ termination_by n => n
 
 /--
 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) : ∀ (a : Nat), motive a
+  (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
@@ -212,7 +212,7 @@ termination_by n => n
 
 /--
 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) : ∀ (a : Nat), motive a
+  (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check with_match_refining_tailrec.induct
@@ -228,7 +228,7 @@ termination_by i
 /--
 info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (i : Nat), motive i 0)
   (case2 : ∀ (n : Nat), motive 0 n.succ) (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i n.succ)
-  (i : Nat) : ∀ (a : Nat), motive i a
+  (i a✝ : Nat) : motive i a✝
 -/
 #guard_msgs in
 #check with_arg_refining_match1.induct
@@ -260,7 +260,7 @@ termination_by n => n
 /--
 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) : ∀ (a : Nat), motive a
+  (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
@@ -274,8 +274,8 @@ termination_by n => n
 
 /--
 info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (a a_1 x : Nat), motive 0 x a a_1)
-  (case2 : ∀ (a a_1 a_2 x : Nat), motive a_2 x (a % 2) (a_1 % 2) → motive a_2.succ x a a_1) :
-  ∀ (a a_1 a_2 a_3 : Nat), motive a a_1 a_2 a_3
+  (case2 : ∀ (a a_1 a_2 x : Nat), motive a_2 x (a % 2) (a_1 % 2) → motive a_2.succ x a a_1) (a✝ a✝¹ a✝² a✝³ : Nat) :
+  motive a✝ a✝¹ a✝² a✝³
 -/
 #guard_msgs in
 #check with_mixed_match_tailrec.induct
@@ -293,8 +293,8 @@ termination_by n => n
 /--
 info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop)
   (case1 : ∀ (a a_1 a_2 a_3 : Nat), motive 0 a a_1 a_2 a_3) (case2 : ∀ (a a_1 n x : Nat), motive n.succ 0 x a a_1)
-  (case3 : ∀ (a a_1 n a_2 x : Nat), motive n a_2 x (a % 2) (a_1 % 2) → motive n.succ a_2.succ x a a_1) :
-  ∀ (a a_1 a_2 a_3 a_4 : Nat), motive a a_1 a_2 a_3 a_4
+  (case3 : ∀ (a a_1 n a_2 x : Nat), motive n a_2 x (a % 2) (a_1 % 2) → motive n.succ a_2.succ x a a_1)
+  (a✝ a✝¹ a✝² a✝³ a✝⁴ : Nat) : motive a✝ a✝¹ a✝² a✝³ a✝⁴
 -/
 #guard_msgs in
 #check with_mixed_match_tailrec2.induct
@@ -310,8 +310,8 @@ def with_match_non_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+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
@@ -333,8 +333,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) :
-  ∀ (a : Nat), motive a
+        motive n.succ)
+  (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check with_match_non_tailrec_refining.induct
@@ -350,8 +350,8 @@ termination_by n => n
 
 /--
 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) :
-  ∀ (a : Nat), motive a
+  (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
@@ -368,7 +368,7 @@ termination_by n => n
 
 /--
 info: UnusedExtraParams.unary.induct (base : Nat) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive n.succ) : ∀ (a : Nat), motive a
+  (case2 : ∀ (n : Nat), motive n → motive n.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check unary.induct
@@ -380,7 +380,7 @@ termination_by n => n
 
 /--
 info: UnusedExtraParams.binary.induct (base : Nat) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-  (case2 : ∀ (n m : Nat), motive n m → motive n.succ m) : ∀ (a a_1 : Nat), motive a a_1
+  (case2 : ∀ (n m : Nat), motive n m → motive n.succ m) (a✝ a✝¹ : Nat) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check binary.induct
@@ -512,7 +512,7 @@ def foo {α} (x : α) : List α → Nat
 termination_by xs => xs
 /--
 info: LetFun.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
+  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -527,7 +527,7 @@ termination_by xs => xs
 
 /--
 info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), Nat → motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
+  (case2 : ∀ (_y : α) (ys : List α), Nat → motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
 #check bar.induct
@@ -545,7 +545,7 @@ termination_by n => n
 /--
 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) : ∀ (a : Nat), motive a
+  (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -563,7 +563,7 @@ termination_by n => n
 /--
 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) : ∀ (a : Nat), motive a
+  (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check bar.induct
@@ -585,14 +585,14 @@ end
 
 /--
 info: EvenOdd.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
-  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a : Nat), motive1 a
+  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (a✝ : Nat) : motive1 a✝
 -/
 #guard_msgs in
 #check even.induct
 
 /--
 info: EvenOdd.odd.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
-  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a : Nat), motive2 a
+  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (a✝ : Nat) : motive2 a✝
 -/
 #guard_msgs in
 #check odd.induct
@@ -615,7 +615,7 @@ end
 /--
 info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
   (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts))
-  (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) : ∀ (a : Tree), motive1 a
+  (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (a✝ : Tree) : motive1 a✝
 -/
 #guard_msgs in
 #check Tree.map.induct
@@ -686,8 +686,8 @@ info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop) (c
   (case2 : ∀ (k x : Nat), (x = 0 → False) → ∀ (x_2 : Fin k), motive x 0 k x_2)
   (case3 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 0), motive x x_1 0 a)
   (case4 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 1), motive x x_1 1 a)
-  (case5 : ∀ (n m k : Nat) (a : Fin k.succ.succ), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ a) :
-  ∀ (a a_1 k : Nat) (a_2 : Fin k), motive a a_1 k a_2
+  (case5 : ∀ (n m k : Nat) (a : Fin k.succ.succ), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ a)
+  (a✝ a✝¹ k : Nat) (a✝² : Fin k) : motive a✝ a✝¹ k a✝²
 -/
 #guard_msgs in
 #check foo.induct
@@ -739,7 +739,7 @@ termination_by n => n
 /--
 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) : ∀ (a : Nat), motive a
+  (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
diff --git a/tests/lean/run/namePatEqThm.lean b/tests/lean/run/namePatEqThm.lean
index a618088387..28be818706 100644
--- a/tests/lean/run/namePatEqThm.lean
+++ b/tests/lean/run/namePatEqThm.lean
@@ -26,10 +26,8 @@ info: f.eq_2 (x_1 y : Nat) (zs : List Nat) (x_2 : zs = [] → False) : f (x_1 ::
 #check f.eq_2
 
 /--
-info: f.eq_3 :
-  ∀ (x : List Nat),
-    (∀ (x_1 y : Nat), x = [x_1, y] → False) →
-      (∀ (x_1 y : Nat) (zs : List Nat), x = x_1 :: y :: zs → False) → f x = ([], [])
+info: f.eq_3 (x✝ : List Nat) (x_2 : ∀ (x y : Nat), x✝ = [x, y] → False)
+  (x_3 : ∀ (x y : Nat) (zs : List Nat), x✝ = x :: y :: zs → False) : f x✝ = ([], [])
 -/
 #guard_msgs in
 #check f.eq_3
diff --git a/tests/lean/run/reserved.lean b/tests/lean/run/reserved.lean
index 97540a421c..8b8ba0de93 100644
--- a/tests/lean/run/reserved.lean
+++ b/tests/lean/run/reserved.lean
@@ -40,12 +40,11 @@ def nonrecfun : Bool → Nat
   | true => 0
 
 /--
-info: nonrecfun.eq_def :
-  ∀ (x : Bool),
-    nonrecfun x =
-      match x with
-      | false => 0
-      | true => 0
+info: nonrecfun.eq_def (x✝ : Bool) :
+  nonrecfun x✝ =
+    match x✝ with
+    | false => 0
+    | true => 0
 -/
 #guard_msgs in
 #check nonrecfun.eq_def
@@ -63,12 +62,11 @@ def fact : Nat → Nat
   | n+1 => (n+1) * fact n
 
 /--
-info: fact.eq_def :
-  ∀ (x : Nat),
-    fact x =
-      match x with
-      | 0 => 1
-      | n.succ => (n + 1) * fact n
+info: fact.eq_def (x✝ : Nat) :
+  fact x✝ =
+    match x✝ with
+    | 0 => 1
+    | n.succ => (n + 1) * fact n
 -/
 #guard_msgs in
 #check fact.eq_def
diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean
index 63d7f0a433..cf243b665f 100644
--- a/tests/lean/run/structuralMutual.lean
+++ b/tests/lean/run/structuralMutual.lean
@@ -631,7 +631,7 @@ namespace FunIndTests
 info: A.size.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self)
   (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty)
   (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a))
-  (case6 : motive_2 B.empty) : ∀ (a : A), motive_1 a
+  (case6 : motive_2 B.empty) (a✝ : A) : motive_1 a✝
 -/
 #guard_msgs in
 #check A.size.induct
@@ -649,7 +649,7 @@ info: A.subs.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀
 info: MutualIndNonMutualFun.A.self_size.induct (motive : MutualIndNonMutualFun.A → Prop)
   (case1 : ∀ (a : MutualIndNonMutualFun.A), motive a → motive a.self)
   (case2 : ∀ (a : MutualIndNonMutualFun.B), motive (MutualIndNonMutualFun.A.other a))
-  (case3 : motive MutualIndNonMutualFun.A.empty) : ∀ (a : MutualIndNonMutualFun.A), motive a
+  (case3 : motive MutualIndNonMutualFun.A.empty) (a✝ : MutualIndNonMutualFun.A) : motive a✝
 -/
 #guard_msgs in
 #check MutualIndNonMutualFun.A.self_size.induct
@@ -658,8 +658,8 @@ info: MutualIndNonMutualFun.A.self_size.induct (motive : MutualIndNonMutualFun.A
 info: MutualIndNonMutualFun.A.self_size_with_param.induct (motive : Nat → MutualIndNonMutualFun.A → Prop)
   (case1 : ∀ (n : Nat) (a : MutualIndNonMutualFun.A), motive n a → motive n a.self)
   (case2 : ∀ (x : Nat) (a : MutualIndNonMutualFun.B), motive x (MutualIndNonMutualFun.A.other a))
-  (case3 : ∀ (x : Nat), motive x MutualIndNonMutualFun.A.empty) :
-  ∀ (a : Nat) (a_1 : MutualIndNonMutualFun.A), motive a a_1
+  (case3 : ∀ (x : Nat), motive x MutualIndNonMutualFun.A.empty) (a✝ : Nat) (a✝¹ : MutualIndNonMutualFun.A) :
+  motive a✝ a✝¹
 -/
 #guard_msgs in
 #check MutualIndNonMutualFun.A.self_size_with_param.induct
@@ -668,7 +668,7 @@ info: MutualIndNonMutualFun.A.self_size_with_param.induct (motive : Nat → Mutu
 info: A.hasNoBEmpty.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self)
   (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty)
   (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a))
-  (case6 : motive_2 B.empty) : ∀ (a : A), motive_1 a
+  (case6 : motive_2 B.empty) (a✝ : A) : motive_1 a✝
 -/
 #guard_msgs in
 #check A.hasNoBEmpty.induct
@@ -676,7 +676,7 @@ info: A.hasNoBEmpty.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case
 /--
 info: EvenOdd.isEven.induct (motive_1 motive_2 : Nat → Prop) (case1 : motive_1 0)
   (case2 : ∀ (n : Nat), motive_2 n → motive_1 n.succ) (case3 : motive_2 0)
-  (case4 : ∀ (n : Nat), motive_1 n → motive_2 n.succ) : ∀ (a : Nat), motive_1 a
+  (case4 : ∀ (n : Nat), motive_1 n → motive_2 n.succ) (a✝ : Nat) : motive_1 a✝
 -/
 #guard_msgs in
 #check EvenOdd.isEven.induct
diff --git a/tests/lean/run/unfoldLemma.lean b/tests/lean/run/unfoldLemma.lean
index 01cb1d88a2..ab6f2bd138 100644
--- a/tests/lean/run/unfoldLemma.lean
+++ b/tests/lean/run/unfoldLemma.lean
@@ -12,12 +12,11 @@ theorem Option_map.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α
 #print equations Option_map
 
 /--
-info: Option_map.eq_def.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) :
-  ∀ (x : Option α),
-    Option_map f x =
-      match x with
-      | none => none
-      | some x => some (f x)
+info: Option_map.eq_def.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (x✝ : Option α) :
+  Option_map f x✝ =
+    match x✝ with
+    | none => none
+    | some x => some (f x)
 -/
 #guard_msgs in
 #check Option_map.eq_def
diff --git a/tests/lean/run/wfEqns5.lean b/tests/lean/run/wfEqns5.lean
index 71e48766e6..2e20121a57 100644
--- a/tests/lean/run/wfEqns5.lean
+++ b/tests/lean/run/wfEqns5.lean
@@ -14,15 +14,14 @@ theorem foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
 #print equations foo
 
 /--
-info: foo.eq_def :
-  ∀ (x x_1 : Nat),
-    foo x x_1 =
-      match x, x_1 with
-      | 0, m =>
-        match m with
-        | 0 => 0
-        | m => m
-      | n.succ, m => foo n m
+info: foo.eq_def (x✝ x✝¹ : Nat) :
+  foo x✝ x✝¹ =
+    match x✝, x✝¹ with
+    | 0, m =>
+      match m with
+      | 0 => 0
+      | m => m
+    | n.succ, m => foo n m
 -/
 #guard_msgs in
 #check foo.eq_def
@@ -51,15 +50,14 @@ theorem bar.eq_2 : ∀ (x n : Nat), bar n.succ x = bar n x
 #print equations bar
 
 /--
-info: bar.eq_def :
-  ∀ (x x_1 : Nat),
-    bar x x_1 =
-      match x, x_1 with
-      | 0, m =>
-        match m with
-        | 0 => 0
-        | m => m
-      | n.succ, m => bar n m
+info: bar.eq_def (x✝ x✝¹ : Nat) :
+  bar x✝ x✝¹ =
+    match x✝, x✝¹ with
+    | 0, m =>
+      match m with
+      | 0 => 0
+      | m => m
+    | n.succ, m => bar n m
 -/
 #guard_msgs in
 #check bar.eq_def
@@ -83,15 +81,14 @@ theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
 #print equations foo
 
 /--
-info: Structural.foo.eq_def :
-  ∀ (x x_1 : Nat),
-    foo x x_1 =
-      match x, x_1 with
-      | 0, m =>
-        match m with
-        | 0 => 0
-        | m => m
-      | n.succ, m => foo n m
+info: Structural.foo.eq_def (x✝ x✝¹ : Nat) :
+  foo x✝ x✝¹ =
+    match x✝, x✝¹ with
+    | 0, m =>
+      match m with
+      | 0 => 0
+      | m => m
+    | n.succ, m => foo n m
 -/
 #guard_msgs in
 #check foo.eq_def
@@ -120,15 +117,14 @@ theorem Structural.bar.eq_2 : ∀ (x n : Nat), bar n.succ x = bar n x
 #print equations bar
 
 /--
-info: Structural.bar.eq_def :
-  ∀ (x x_1 : Nat),
-    bar x x_1 =
-      match x, x_1 with
-      | 0, m =>
-        match m with
-        | 0 => 0
-        | m => m
-      | n.succ, m => bar n m
+info: Structural.bar.eq_def (x✝ x✝¹ : Nat) :
+  bar x✝ x✝¹ =
+    match x✝, x✝¹ with
+    | 0, m =>
+      match m with
+      | 0 => 0
+      | m => m
+    | n.succ, m => bar n m
 -/
 #guard_msgs in
 #check bar.eq_def