diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 047662ecbabb..1b4b7cf7cc79 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -1279,7 +1279,7 @@ 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 (opts', e') ← processSpine {} (← readThe SubExpr)
@@ -1295,6 +1295,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⟩
@@ -1320,10 +1321,11 @@ 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:
diff --git a/tests/lean/autoImplicitChainNameIssue.lean.expected.out b/tests/lean/autoImplicitChainNameIssue.lean.expected.out
index f5430942390a..a56d97e58d81 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 α✝} (h : 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 185733340dab..c5afb1731d64 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 α) → (h_1 : (a : α) → motive [a]) → (h_2 : (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 44ca7773c033..5bd6aab0f8f3 100644
--- a/tests/lean/run/2846.lean
+++ b/tests/lean/run/2846.lean
@@ -34,7 +34,7 @@ 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
 
 /-!
@@ -43,11 +43,11 @@ 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✝ : Nat) → (a : Fin (n + 1)) → Fin (n✝ + 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.
+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
@@ -57,12 +57,12 @@ def foo'' : String → (needle : String) → String := fun _ yo => yo
 
 /-!
 Named argument after inaccessible name that's still a dependent argument.
-Stays after the colon, and the names are grouped.
+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✝) -/
+/-- info: foo''' (x✝ n : Nat) : Fin (n + x✝) -/
 #guard_msgs in #check foo'''
 
 /-!
diff --git a/tests/lean/run/4320.lean b/tests/lean/run/4320.lean
index c60bb3afc478..adcdfd4a3d03 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/974.lean b/tests/lean/run/974.lean
index 0953edb43f36..a27878533e56 100644
--- a/tests/lean/run/974.lean
+++ b/tests/lean/run/974.lean
@@ -11,23 +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✝¹ : 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
+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 0937b67f5a32..1d33ae6bb98b 100644
--- a/tests/lean/run/eqnsPrio.lean
+++ b/tests/lean/run/eqnsPrio.lean
@@ -11,15 +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_3 : 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 fb5b635b7d28..deca8f44c630 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✝¹ : Nat), motive a✝ a✝¹
+  (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 dc26e889ac0d..453021165d1c 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 aaf449b03180..f6b24b0c0258 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 731e202e7611..16b959762612 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✝¹ : Nat), motive a✝ a✝¹
+  (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✝¹ : Nat), motive a✝ a✝¹
+  (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✝¹ : List β), motive a✝ a✝¹
+  (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✝¹ : HList Ty.denote ctx), motive a✝ a✝¹
+  {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 662039d15316..8f5825658bd6 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 f64093b37d11..d33297ab6bfb 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✝¹ : Nat), motive a✝ a✝¹
+  (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✝¹ a✝² a✝³ : Nat), motive a✝ a✝¹ a✝² a✝³
+  (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✝¹ a✝² a✝³ a✝⁴ : Nat), motive a✝ a✝¹ a✝² a✝³ a✝⁴
+  (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✝¹ : Nat), motive a✝ a✝¹
+  (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✝¹ k : Nat) (a✝² : Fin k), motive a✝ a✝¹ k 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✝¹ 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 043ffd41e4a8..28be81870646 100644
--- a/tests/lean/run/namePatEqThm.lean
+++ b/tests/lean/run/namePatEqThm.lean
@@ -26,9 +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_2 : ∀ (x y : Nat), x✝ = [x, y] → False)
-    (x_3 : ∀ (x y : Nat) (zs : List Nat), x✝ = x :: 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 83e2c90b7c74..8b8ba0de934a 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 5c677ec7dc72..cf243b665f26 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✝¹ : MutualIndNonMutualFun.A), motive a✝ a✝¹
+  (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 38f34907f1d0..ab6f2bd138ca 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 a95218e5cb9e..2e20121a5797 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✝¹ : Nat),
-    foo x✝ x✝¹ =
-      match x✝, x✝¹ 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✝¹ : Nat),
-    bar x✝ x✝¹ =
-      match x✝, x✝¹ 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✝¹ : Nat),
-    foo x✝ x✝¹ =
-      match x✝, x✝¹ 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✝¹ : Nat),
-    bar x✝ x✝¹ =
-      match x✝, x✝¹ 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