diff --git a/tests/lean/438.lean.expected.out b/tests/lean/438.lean.expected.out
index a25800c7f..03b9d32c8 100644
--- a/tests/lean/438.lean.expected.out
+++ b/tests/lean/438.lean.expected.out
@@ -12,5 +12,5 @@ P : group P₀
 ⊢ ?M_1
 438.lean:10:2: error: failed to add declaration 'lambda_morphism.mk' to environment, type has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  Π {P₀ : Type} {P : …},
+  Π {P₀} {P},
     ?M_2 = ?M_3 → …
diff --git a/tests/lean/480.hlean.expected.out b/tests/lean/480.hlean.expected.out
index e5f78aefc..02f0a29ef 100644
--- a/tests/lean/480.hlean.expected.out
+++ b/tests/lean/480.hlean.expected.out
@@ -1 +1 @@
-is_contr.mk : Π (center : ?A), (Π (a : ?A), center = a) → is_contr ?A
+is_contr.mk : Π center, (Π a, center = a) → is_contr ?A
diff --git a/tests/lean/487.hlean.expected.out b/tests/lean/487.hlean.expected.out
index e084b8555..d62de691a 100644
--- a/tests/lean/487.hlean.expected.out
+++ b/tests/lean/487.hlean.expected.out
@@ -3,10 +3,10 @@ A : Type,
 B : Type,
 f : A → B,
 g : B → A,
-ε : Π (b : B), f (g b) = b,
+ε : Π b, f (g b) = b,
 b b' : B
 ⊢ (ε b)⁻¹ ⬝ ε b = refl b
 487.hlean:19:0: error: failed to add declaration 'foo' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (B : Type) (f : …) (g : …) (ε : …) (b b' : B),
+  λ A B f g ε b b',
     is_retraction.mk … ?M_1
diff --git a/tests/lean/550.lean.expected.out b/tests/lean/550.lean.expected.out
index 49cfc7644..a9bf52e4f 100644
--- a/tests/lean/550.lean.expected.out
+++ b/tests/lean/550.lean.expected.out
@@ -32,5 +32,5 @@ rinv : func ∘ finv = id
 ⊢ inv (mk func finv linv rinv) ∘b mk func finv linv rinv = id
 550.lean:43:2: error: failed to add declaration 'bijection.inv.linv' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (f : …),
+  λ A f,
     bijection.rec_on f ?M_1
diff --git a/tests/lean/571.lean.expected.out b/tests/lean/571.lean.expected.out
index 16e0b502f..90df22f38 100644
--- a/tests/lean/571.lean.expected.out
+++ b/tests/lean/571.lean.expected.out
@@ -1,11 +1,11 @@
 571.lean:6:2: error:invalid 'cases' tactic, 'Exists' can only eliminate to Prop
 proof state:
 P : ℕ → Prop,
-H : ∃ (n : ℕ), P n
+H : ∃ n, P n
 ⊢ ℕ
 571.lean:7:0: error: don't know how to synthesize placeholder
 P : ℕ → Prop,
-H : ∃ (n : ℕ), P n
+H : ∃ n, P n
 ⊢ ℕ
 571.lean:7:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
diff --git a/tests/lean/583.lean.expected.out b/tests/lean/583.lean.expected.out
index 4355b2dd0..0bfe4cfb3 100644
--- a/tests/lean/583.lean.expected.out
+++ b/tests/lean/583.lean.expected.out
@@ -10,5 +10,5 @@ P : f a⁻¹ * f a = 1
 ⊢ f a⁻¹ = (f a)⁻¹
 583.lean:27:8: error: failed to add declaration 'group_hom.hom_map_inv' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (B : Type) (s1 : …) (s2 : …) (f : …) (Hom : …) (a : A),
+  λ A B s1 s2 f Hom a,
     ?M_1 …
diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out
index 20737e6b3..886bfa8b8 100644
--- a/tests/lean/584a.lean.expected.out
+++ b/tests/lean/584a.lean.expected.out
@@ -1,5 +1,5 @@
-foo : Π (A : Type) [H : inhabited A], A → A
-foo' : Π {A : Type} [H : inhabited A] {x : A}, A
+foo : Π A [H], A → A
+foo' : Π {A} [H] {x}, A
 foo ℕ 10 : ℕ
 definition test : ∀ {A : Type} [H : inhabited A], @foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5) = 10 :=
-λ (A : Type) (H : inhabited A), @rfl ℕ (@foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5))
+λ A H, @rfl ℕ (@foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5))
diff --git a/tests/lean/584b.lean.expected.out b/tests/lean/584b.lean.expected.out
index 6fd6153f0..0a8f08edf 100644
--- a/tests/lean/584b.lean.expected.out
+++ b/tests/lean/584b.lean.expected.out
@@ -1,4 +1,4 @@
-tst₁ : Π (A : Type), A → A
-tst₂ : Π {A : Type}, A → A
-symm₂ : ∀ {A : Type} (a b : A), a = b → b = a
-tst₃ : Π (A : Type), A → A
+tst₁ : Π A, A → A
+tst₂ : Π {A}, A → A
+symm₂ : ∀ {A} a b, a = b → b = a
+tst₃ : Π A, A → A
diff --git a/tests/lean/584c.lean.expected.out b/tests/lean/584c.lean.expected.out
index 30a049fce..a3d2a6544 100644
--- a/tests/lean/584c.lean.expected.out
+++ b/tests/lean/584c.lean.expected.out
@@ -1,5 +1,5 @@
-tst₁ : Π (A : Type), A → A
-tst₂ : Π {A : Type}, A → A
-symm₂ : ∀ {A : Type} (a b : A), a = b → b = a
-tst₃ : Π (A : Type), A → A
-foo : ∀ {A : Type} {a b : A}, a = b → (∀ (c : A), c = b → c = a)
+tst₁ : Π A, A → A
+tst₂ : Π {A}, A → A
+symm₂ : ∀ {A} a b, a = b → b = a
+tst₃ : Π A, A → A
+foo : ∀ {A} {a b}, a = b → (∀ c, c = b → c = a)
diff --git a/tests/lean/587.lean.expected.out b/tests/lean/587.lean.expected.out
index a73cb1530..6fc3a162f 100644
--- a/tests/lean/587.lean.expected.out
+++ b/tests/lean/587.lean.expected.out
@@ -2,7 +2,7 @@
 A B : Type₁,
 s : setoid A,
 f : A → B,
-c : ∀ (a₁ a₂ : A), a₁ ≈ a₂ → f a₁ = f a₂,
+c : ∀ a₁ a₂, a₁ ≈ a₂ → f a₁ = f a₂,
 a : A,
 g h : B → B,
 gh : g = h
diff --git a/tests/lean/608.hlean.expected.out b/tests/lean/608.hlean.expected.out
index 31f30db69..4f5151aa2 100644
--- a/tests/lean/608.hlean.expected.out
+++ b/tests/lean/608.hlean.expected.out
@@ -1,11 +1,11 @@
 definition id [reducible] [unfold_full] : Π {A : Type}, A → A :=
-λ (A : Type) (a : A), a
+λ A a, a
 
 definition category.id [reducible] [unfold 1] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a :=
 ID
 -----------
 definition id [reducible] [unfold_full] : Π {A : Type}, A → A
-λ (A : Type) (a : A), a
+λ A a, a
 
 definition category.id [reducible] [unfold 1] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a
 ID
diff --git a/tests/lean/626b.hlean.expected.out b/tests/lean/626b.hlean.expected.out
index 8d718f68b..18e707b25 100644
--- a/tests/lean/626b.hlean.expected.out
+++ b/tests/lean/626b.hlean.expected.out
@@ -3,8 +3,8 @@ x : S¹
 ⊢ bool
 626b.hlean:4:50: error: don't know how to synthesize placeholder
 x : S¹
-⊢ eq.pathover (λ (a : S¹), bool) ?M_1 loop ?M_1
+⊢ eq.pathover (λ a, bool) ?M_1 loop ?M_1
 626b.hlean:4:32: error: failed to add declaration 'f' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (x : S¹),
+  λ x,
     circle.rec_on x ?M_1 ?M_2
diff --git a/tests/lean/630.lean.expected.out b/tests/lean/630.lean.expected.out
index 39a1ffa02..df473450f 100644
--- a/tests/lean/630.lean.expected.out
+++ b/tests/lean/630.lean.expected.out
@@ -1,5 +1,5 @@
 definition pnat.pnat : Type₁ :=
-{n : ℕ | n > 0}
+{n | n > 0}
 inductive prod : Type → Type → Type
 constructors:
-prod.mk : Π {A : Type} {B : Type}, A → B → A × B
+prod.mk : Π {A} {B}, A → B → A × B
diff --git a/tests/lean/634d.lean.expected.out b/tests/lean/634d.lean.expected.out
index a942294a2..fca3c316a 100644
--- a/tests/lean/634d.lean.expected.out
+++ b/tests/lean/634d.lean.expected.out
@@ -3,8 +3,8 @@ _root_.A : Type₁ → Type₁
 A : Type.{l} → Type.{l}
 _root_.A.{1} : Type₁ → Type₁
 P : B → B
-_root_.P : Π {n : ℕ}, ℕ → ℕ
+_root_.P : Π {n}, ℕ → ℕ
 P : B → B
 _root_.P.{1} : ?B → ?B
 @P 2 : B → B
-@_root_.P.{1} ℕ : Π {n : ℕ}, ℕ → ℕ
+@_root_.P.{1} ℕ : Π {n}, ℕ → ℕ
diff --git a/tests/lean/640.hlean.expected.out b/tests/lean/640.hlean.expected.out
index 2a713b0fb..a9c208284 100644
--- a/tests/lean/640.hlean.expected.out
+++ b/tests/lean/640.hlean.expected.out
@@ -2,9 +2,7 @@
 P : quotient S → Type,
 c c' : C,
 a : A
-⊢ pathover P (quotient.rec (λ (b : A), sorry) (λ (b b' : A) (H : R b b'), sorry) (f a unit.star))
-    (eq_of_rel S (S.Rmk a unit.star))
-    sorry
+⊢ pathover P (quotient.rec (λ b, sorry) (λ b b' H, sorry) (f a unit.star)) (eq_of_rel S (S.Rmk a unit.star)) sorry
 640.hlean:25:22: proof state
 P : quotient S → Type,
 c c' : C,
diff --git a/tests/lean/640b.lean.expected.out b/tests/lean/640b.lean.expected.out
index e4a2c47cc..ce37f00e1 100644
--- a/tests/lean/640b.lean.expected.out
+++ b/tests/lean/640b.lean.expected.out
@@ -1 +1 @@
-eq : Π {A : Type}, A → A → Prop
+eq : Π {A}, A → A → Prop
diff --git a/tests/lean/644.lean.expected.out b/tests/lean/644.lean.expected.out
index 0567b0bcb..0a6ae8d79 100644
--- a/tests/lean/644.lean.expected.out
+++ b/tests/lean/644.lean.expected.out
@@ -1,4 +1,4 @@
 f (coe a) : B
-g (λ (x : C), coe (h x)) : B
-filter (λ (x : bool), bool_to_Prop (negb x)) [tt, ff, tt, ff] : list bool
+g (λ x, coe (h x)) : B
+filter (λ x, bool_to_Prop (negb x)) [tt, ff, tt, ff] : list bool
 [ff, ff]
diff --git a/tests/lean/652.lean.expected.out b/tests/lean/652.lean.expected.out
index 27fd63b3d..d9a63a9c7 100644
--- a/tests/lean/652.lean.expected.out
+++ b/tests/lean/652.lean.expected.out
@@ -1,6 +1,6 @@
-R : Π {b c : bool}, Prop
+R : Π {b c}, Prop
 R2 : bool → bool → Prop
 R3 : bool → bool → Prop
-R4 : bool → (Π {c : bool}, Prop)
-R5 : Π {b c : bool}, Prop
-R6 : Π {b : bool}, bool → Prop
+R4 : bool → (Π {c}, Prop)
+R5 : Π {b c}, Prop
+R6 : Π {b}, bool → Prop
diff --git a/tests/lean/669.lean.expected.out b/tests/lean/669.lean.expected.out
index b1811a778..6761aec18 100644
--- a/tests/lean/669.lean.expected.out
+++ b/tests/lean/669.lean.expected.out
@@ -6,7 +6,7 @@ but is expected to have type
   Prop
 the assignment was attempted when processing
     application type constraint
-      (λ {T : Prop} (t : T), t) bool.tt
+      (λ {T} t, t) bool.tt
     term
       bool.tt
     has type
diff --git a/tests/lean/671.lean.expected.out b/tests/lean/671.lean.expected.out
index 8e8eba1fc..9780d4a6e 100644
--- a/tests/lean/671.lean.expected.out
+++ b/tests/lean/671.lean.expected.out
@@ -1,2 +1,2 @@
 protected definition nat.add : ℕ → ℕ → ℕ :=
-λ (a : ℕ), nat.rec a (λ (b₁ : ℕ), nat.succ)
+λ a, nat.rec a (λ b₁, nat.succ)
diff --git a/tests/lean/690.hlean.expected.out b/tests/lean/690.hlean.expected.out
index 603fce6f0..947df0ead 100644
--- a/tests/lean/690.hlean.expected.out
+++ b/tests/lean/690.hlean.expected.out
@@ -12,7 +12,7 @@ q : u₂ =[p] v₂
 690.hlean:12:0: error: don't know how to synthesize placeholder
 A : Type,
 B : A → Type,
-u v : Σ (a : A), B a,
+u v : Σ a, B a,
 p : u.1 = v.1,
 q : u.2 =[p] v.2
 ⊢ ⟨(sigma_eq p q)..1, (sigma_eq p q)..2⟩ = ⟨p, q⟩
diff --git a/tests/lean/775.lean.expected.out b/tests/lean/775.lean.expected.out
index 67acb60cc..f713bdac5 100644
--- a/tests/lean/775.lean.expected.out
+++ b/tests/lean/775.lean.expected.out
@@ -11,13 +11,13 @@ p : P 0 (succ a)
 
 P Q : ℕ → ℕ → Prop,
 a : ℕ,
-v_0 : ∀ (m : ℕ), P a m → Q a m,
+v_0 : ∀ m, P a m → Q a m,
 p : P (succ a) 0
 ⊢ Q (succ a) 0
 
 P Q : ℕ → ℕ → Prop,
 a : ℕ,
-v_0 : ∀ (m : ℕ), P a m → Q a m,
+v_0 : ∀ m, P a m → Q a m,
 a_1 : ℕ,
 v_0_1 : P (succ a) a_1 → Q (succ a) a_1,
 p : P (succ a) (succ a_1)
diff --git a/tests/lean/779.hlean.expected.out b/tests/lean/779.hlean.expected.out
index c169894a5..89a227ea5 100644
--- a/tests/lean/779.hlean.expected.out
+++ b/tests/lean/779.hlean.expected.out
@@ -1,2 +1,2 @@
 definition foo : empty → empty :=
-empty.rec (λ (e : empty), empty)
+empty.rec (λ e, empty)
diff --git a/tests/lean/abbrev1.lean.expected.out b/tests/lean/abbrev1.lean.expected.out
index 984ab8f94..673c6b9d9 100644
--- a/tests/lean/abbrev1.lean.expected.out
+++ b/tests/lean/abbrev1.lean.expected.out
@@ -1,6 +1,6 @@
 definition tst : ℕ
-(λ (a : Type₁), 2 + 3) ℕ
+(λ a, 2 + 3) ℕ
 definition tst : ℕ
 foo ℕ
 definition tst1 : ℕ
-(λ (A : Type₁) (a : A), a) ℕ 10
+(λ A a, a) ℕ 10
diff --git a/tests/lean/acc.lean.expected.out b/tests/lean/acc.lean.expected.out
index 6fabcafe2..8a07895d1 100644
--- a/tests/lean/acc.lean.expected.out
+++ b/tests/lean/acc.lean.expected.out
@@ -1,4 +1,3 @@
 acc.rec :
-  Π {A : Type} {R : A → A → Prop} {C : A → Type},
-    (Π (x : A), (∀ (y : A), R y x → acc A R y) → (Π (y : A), R y x → C y) → C x) →
-    (Π {a : A}, acc A R a → C a)
+  Π {A} {R} {C},
+    (Π x, (∀ y, R y x → acc A R y) → (Π y, R y x → C y) → C x) → (Π {a}, acc A R a → C a)
diff --git a/tests/lean/acc_rec_bug.lean.expected.out b/tests/lean/acc_rec_bug.lean.expected.out
index 2a8d7ac3a..4f14ebe72 100644
--- a/tests/lean/acc_rec_bug.lean.expected.out
+++ b/tests/lean/acc_rec_bug.lean.expected.out
@@ -1,12 +1,3 @@
-F x₁
-  (λ (y : A) (a : R y x₁),
-     acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH)
-       (ac y a))
-acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH)
-  (acc.intro x₁ ac) :
-  C x₁
-F x₁
-  (λ (y : A) (a : R y x₁),
-     acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH)
-       (ac y a)) :
-  C x₁
+F x₁ (λ y a, acc.rec (λ x₂ ac iH, F x₂ iH) (ac y a))
+acc.rec (λ x₂ ac iH, F x₂ iH) (acc.intro x₁ ac) : C x₁
+F x₁ (λ y a, acc.rec (λ x₂ ac iH, F x₂ iH) (ac y a)) : C x₁
diff --git a/tests/lean/attr_at1.lean.expected.out b/tests/lean/attr_at1.lean.expected.out
index 62ad7a2b7..3f47a8ee9 100644
--- a/tests/lean/attr_at1.lean.expected.out
+++ b/tests/lean/attr_at1.lean.expected.out
@@ -1,8 +1,8 @@
 definition f : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition f [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition f : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition f [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
diff --git a/tests/lean/attr_at2.lean.expected.out b/tests/lean/attr_at2.lean.expected.out
index ecbee7757..0b344e7a6 100644
--- a/tests/lean/attr_at2.lean.expected.out
+++ b/tests/lean/attr_at2.lean.expected.out
@@ -1,35 +1,35 @@
 sec 3. 
 definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + a
+λ a, a + a
 sec 2. 
 definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + a
+λ a, a + a
 sec 1. 
 definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + a
+λ a, a + a
 foo.bah.bla. 
 definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + a
+λ a, a + a
 foo.bah. 
 definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + a
+λ a, a + a
 foo. 
 definition foo.bah.bla.f : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + a
+λ a, a + a
 root. 
 definition foo.bah.bla.f : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + a
+λ a, a + a
diff --git a/tests/lean/attr_at3.lean.expected.out b/tests/lean/attr_at3.lean.expected.out
index 7805bcc88..aaa35eba8 100644
--- a/tests/lean/attr_at3.lean.expected.out
+++ b/tests/lean/attr_at3.lean.expected.out
@@ -1,8 +1,8 @@
 definition bla.f : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition bla.f [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition bla.f : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
 definition bla.f [reducible] : ℕ → ℕ :=
-λ (a : ℕ), a + 1
+λ a, a + 1
diff --git a/tests/lean/auto_include.lean.expected.out b/tests/lean/auto_include.lean.expected.out
index 856b99dcd..26bdba0f4 100644
--- a/tests/lean/auto_include.lean.expected.out
+++ b/tests/lean/auto_include.lean.expected.out
@@ -1,8 +1,8 @@
 definition foo : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=
-λ (A : Type) (_inst_1 : group A) (a b : A), sorry
+λ A _inst_1 a b, sorry
 definition bla : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=
-λ (B : Type) (_inst_2 : group B) (b : B), sorry
+λ B _inst_2 b, sorry
 definition foo2 : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=
-λ (A : Type) (_inst_1 : group A) (a b : A), sorry
+λ A _inst_1 a b, sorry
 definition bla2 : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=
-λ (B : Type) (_inst_2 : group B) (b : B), sorry
+λ B _inst_2 b, sorry
diff --git a/tests/lean/binder_overload.lean.expected.out b/tests/lean/binder_overload.lean.expected.out
index 6adfc8960..5be3e011a 100644
--- a/tests/lean/binder_overload.lean.expected.out
+++ b/tests/lean/binder_overload.lean.expected.out
@@ -1,15 +1,15 @@
-{x : ℕ ∈ S | x > 0} : set ℕ
-{x : ℕ ∈ s | x > 0} : finset ℕ
+{x ∈ S | x > 0} : set ℕ
+{x ∈ s | x > 0} : finset ℕ
 @set.sep.{1} nat
-  (λ (x : nat),
+  (λ x,
      @gt.{1} nat nat._trans_of_decidable_linear_ordered_semiring_13 x
        (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6))
   S :
   set.{1} nat
-@finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b)
-  (λ (x : nat),
+@finset.sep.{1} nat (λ a b, nat.has_decidable_eq a b)
+  (λ x,
      @gt.{1} nat nat._trans_of_decidable_linear_ordered_semiring_13 x
        (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6))
-  (λ (a : nat), nat.decidable_lt (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6) a)
+  (λ a, nat.decidable_lt (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6) a)
   s :
   finset.{1} nat
diff --git a/tests/lean/blast_back2.lean.expected.out b/tests/lean/blast_back2.lean.expected.out
index 6c1b57996..b5c20ba73 100644
--- a/tests/lean/blast_back2.lean.expected.out
+++ b/tests/lean/blast_back2.lean.expected.out
@@ -1,4 +1,4 @@
 definition lemma1 : ∀ (a : ℕ), r a → s a → p a :=
-λ (a : ℕ) (H.1 : r a) (H.2 : s a), rq₁ a H.1
+λ a H.1 H.2, rq₁ a H.1
 definition lemma2 : ∀ (a : ℕ), r a → s a → p a :=
-λ (a : ℕ) (H.1 : r a), rq₂ a
+λ a H.1, rq₂ a
diff --git a/tests/lean/blast_cc_not_provable.lean.expected.out b/tests/lean/blast_cc_not_provable.lean.expected.out
index d1242d7cb..24580a5bc 100644
--- a/tests/lean/blast_cc_not_provable.lean.expected.out
+++ b/tests/lean/blast_cc_not_provable.lean.expected.out
@@ -2,7 +2,7 @@ blast_cc_not_provable.lean:5:0: error: blast tactic failed
 strategy 'cc' failed, no proof found, final state:
 C : ℕ → Type,
 n m : ℕ,
-f : Π (n : ℕ), C n → C n,
+f : Π n, C n → C n,
 c : C n,
 d : C m,
 H.6 : f n == f m,
@@ -11,14 +11,14 @@ H.7 : c == d
 -------
 proof state:
 C : ℕ → Type,
-f : Π (n : ℕ), C n → C n,
+f : Π n, C n → C n,
 n m : ℕ,
 c : C n,
 d : C m
 ⊢ f n == f m → c == d → f n c == f m d
 blast_cc_not_provable.lean:5:0: error: don't know how to synthesize placeholder
 C : ℕ → Type,
-f : Π (n : ℕ), C n → C n,
+f : Π n, C n → C n,
 n m : ℕ,
 c : C n,
 d : C m
diff --git a/tests/lean/bug1.lean.expected.out b/tests/lean/bug1.lean.expected.out
index 6f19cf6b8..9df9a7d84 100644
--- a/tests/lean/bug1.lean.expected.out
+++ b/tests/lean/bug1.lean.expected.out
@@ -1,19 +1,19 @@
 bug1.lean:9:7: error: type mismatch at definition 'and_intro1', has type
-  ∀ (p q : bool),
-    p → q → (∀ (c : bool), (p → q → c) → c)
+  ∀ p q,
+    p → q → (∀ c, (p → q → c) → c)
 but is expected to have type
-  ∀ (p q : bool),
+  ∀ p q,
     p → q → a
 bug1.lean:13:7: error: type mismatch at definition 'and_intro2', has type
-  ∀ (p q : bool),
-    p → q → (∀ (c : bool), (p → q → c) → c)
+  ∀ p q,
+    p → q → (∀ c, (p → q → c) → c)
 but is expected to have type
-  ∀ (p q : bool),
+  ∀ p q,
     p → q → p ∧ p
 bug1.lean:17:7: error: type mismatch at definition 'and_intro3', has type
-  ∀ (p q : bool),
-    p → q → (∀ (c : bool), (p → q → c) → c)
+  ∀ p q,
+    p → q → (∀ c, (p → q → c) → c)
 but is expected to have type
-  ∀ (p q : bool),
+  ∀ p q,
     p → q → q ∧ p
-and_intro4 : ∀ (p q : bool), p → q → p ∧ q
+and_intro4 : ∀ p q, p → q → p ∧ q
diff --git a/tests/lean/calc_assistant.lean.expected.out b/tests/lean/calc_assistant.lean.expected.out
index 3c01c5299..3da3b5735 100644
--- a/tests/lean/calc_assistant.lean.expected.out
+++ b/tests/lean/calc_assistant.lean.expected.out
@@ -1,7 +1,7 @@
 calc_assistant.lean:7:14: error: type mismatch at term
   H₁
 has type
-  ∀ (x : num),
+  ∀ x,
     b = x
 but is expected to have type
   a = b
diff --git a/tests/lean/cases_failure.hlean.expected.out b/tests/lean/cases_failure.hlean.expected.out
index 37dfc8970..1129f8914 100644
--- a/tests/lean/cases_failure.hlean.expected.out
+++ b/tests/lean/cases_failure.hlean.expected.out
@@ -5,8 +5,7 @@ auxiliary goal at time of failure
   b r t l : z = z,
   s : square t b l r,
   e_3 : z = z
-  ⊢ Π (e_4 : eq.rec t (refl z) = idp) (e_5 : eq.rec (eq.rec b (refl z)) e_3 = idp) (e_6 : eq.rec l (refl z) = idp)
-    (e_7 : eq.rec (eq.rec r (refl z)) e_3 = idp),
+  ⊢ Π e_4 e_5 e_6 e_7,
       eq.rec (eq.rec (eq.rec (eq.rec (eq.rec (eq.rec (eq.rec s (refl z)) (refl z)) e_3) e_4) e_5) e_6)
         e_7 = square.ids →
       unit
diff --git a/tests/lean/check.lean.expected.out b/tests/lean/check.lean.expected.out
index 34ad91a3f..d156f854c 100644
--- a/tests/lean/check.lean.expected.out
+++ b/tests/lean/check.lean.expected.out
@@ -1,4 +1,4 @@
 and.intro : ?a → ?b → ?a ∧ ?b
 or.elim : ?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c
 eq : ?A → ?A → Prop
-eq.rec : ?C ?a → (Π {a : ?A}, ?a = a → ?C a)
+eq.rec : ?C ?a → (Π {a}, ?a = a → ?C a)
diff --git a/tests/lean/choice_expl.lean.expected.out b/tests/lean/choice_expl.lean.expected.out
index e1274a3f7..19e6b799f 100644
--- a/tests/lean/choice_expl.lean.expected.out
+++ b/tests/lean/choice_expl.lean.expected.out
@@ -1,3 +1,3 @@
-pr : Π {A : Type}, A → A → A
+pr : Π {A}, A → A → A
 pr a b : N
 pr a b : N
diff --git a/tests/lean/coe2.lean.expected.out b/tests/lean/coe2.lean.expected.out
index 9a3a29634..cac2c33fc 100644
--- a/tests/lean/coe2.lean.expected.out
+++ b/tests/lean/coe2.lean.expected.out
@@ -1,5 +1,5 @@
 f (int.of_nat a) : int
-λ (x : bv a), @g a x : bv a → bv a
+λ x, @g a x : bv a → bv a
 coe2.lean:19:6: error: type mismatch at application
   f a
 term
diff --git a/tests/lean/congr_print.lean.expected.out b/tests/lean/congr_print.lean.expected.out
index a7c474dbd..1be643111 100644
--- a/tests/lean/congr_print.lean.expected.out
+++ b/tests/lean/congr_print.lean.expected.out
@@ -1,19 +1,15 @@
 theorem perm.perm_erase_dup_of_perm [congr] : ∀ {A : Type} [H : decidable_eq A] {l₁ l₂ : list A}, l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ :=
-λ (A : Type) (H : decidable_eq A) (l₁ l₂ : list A) (p : l₁ ~ l₂),
+λ A H l₁ l₂ p,
   perm_induction_on p nil
-    (λ (x : A) (t₁ t₂ : list A) (p : t₁ ~ t₂) (r : erase_dup t₁ ~ erase_dup t₂),
-       decidable.by_cases (λ (xint₁ : x ∈ t₁), have xint₂ : x ∈ t₂, from mem_of_mem_erase_dup …, … …)
-         (λ (nxint₁ : x ∉ t₁),
-            have nxint₂ : x ∉ t₂, from λ (xint₂ : x ∈ t₂), … nxint₁,
-            eq.rec … (eq.symm …)))
-    (λ (y x : A) (t₁ t₂ : list A) (p : t₁ ~ t₂) (r : erase_dup t₁ ~ erase_dup t₂),
+    (λ x t₁ t₂ p r,
+       decidable.by_cases (λ xint₁, have xint₂ : x ∈ t₂, from mem_of_mem_erase_dup …, … …)
+         (λ nxint₁, have nxint₂ : x ∉ t₂, from λ xint₂, … nxint₁, eq.rec … (eq.symm …)))
+    (λ y x t₁ t₂ p r,
        decidable.by_cases
-         (λ (xinyt₁ : x ∈ y :: t₁),
-            decidable.by_cases (λ (yint₁ : …), …)
-              (λ (nyint₁ : y ∉ t₁), have nyint₂ : …, from …, …))
-         (λ (nxinyt₁ : x ∉ y :: t₁),
+         (λ xinyt₁, decidable.by_cases (λ yint₁, …) (λ nyint₁, have nyint₂ : …, from …, …))
+         (λ nxinyt₁,
             have xney : x ≠ y, from ne_of_not_mem_cons nxinyt₁,
             have nxint₁ : x ∉ t₁, from not_mem_of_not_mem_cons nxinyt₁,
-            have nxint₂ : x ∉ t₂, from λ (xint₂ : …), …,
+            have nxint₂ : x ∉ t₂, from λ xint₂, …,
             … …))
-    (λ (t₁ t₂ t₃ : list A) (p₁ : t₁ ~ t₂) (p₂ : t₂ ~ t₃), trans)
+    (λ t₁ t₂ t₃ p₁ p₂, trans)
diff --git a/tests/lean/defeq_simplifier1.lean.expected.out b/tests/lean/defeq_simplifier1.lean.expected.out
index e1d570060..673beb6a5 100644
--- a/tests/lean/defeq_simplifier1.lean.expected.out
+++ b/tests/lean/defeq_simplifier1.lean.expected.out
@@ -1,8 +1,8 @@
-λ (x y z w : A), q (q (q w))
-A → A → A → (∀ (w : A), q (q (q w)) = w)
-λ (x y z w : A), q (f (q (q x)) (q (q z)) (q w))
-∀ (x : A), A → (∀ (z w : A), q (f (q (q x)) (q (q z)) (q w)) = w)
-λ (x y z w : A), q (q (q w))
-A → A → A → (∀ (w : A), q (q (q w)) = w)
-λ (x y z w : A), w
-A → A → A → (∀ (w : A), w = w)
+λ x y z w, q (q (q w))
+A → A → A → (∀ w, q (q (q w)) = w)
+λ x y z w, q (f (q (q x)) (q (q z)) (q w))
+∀ x, A → (∀ z w, q (f (q (q x)) (q (q z)) (q w)) = w)
+λ x y z w, q (q (q w))
+A → A → A → (∀ w, q (q (q w)) = w)
+λ x y z w, w
+A → A → A → (∀ w, w = w)
diff --git a/tests/lean/eq_class_error.lean.expected.out b/tests/lean/eq_class_error.lean.expected.out
index 28e650db7..4a07f12b6 100644
--- a/tests/lean/eq_class_error.lean.expected.out
+++ b/tests/lean/eq_class_error.lean.expected.out
@@ -1,7 +1,7 @@
 eq_class_error.lean:15:10: error: don't know how to synthesize placeholder
-decidable_eq_foo : Π (f₁ f₂ : foo), decidable (f₁ = f₂)
+decidable_eq_foo : Π f₁ f₂, decidable (f₁ = f₂)
 ⊢ decidable (b = b)
 eq_class_error.lean:9:11: error: failed to synthesize placeholder
 
-⊢ Π (f₁ f₂ : foo),
+⊢ Π f₁ f₂,
     decidable (f₁ = f₂)
diff --git a/tests/lean/error_pos_bug.lean.expected.out b/tests/lean/error_pos_bug.lean.expected.out
index 3f7535ea7..568be2869 100644
--- a/tests/lean/error_pos_bug.lean.expected.out
+++ b/tests/lean/error_pos_bug.lean.expected.out
@@ -1,5 +1,5 @@
 error_pos_bug.lean:9:0: error: type error in placeholder assigned to
-  λ (a : Category) (b : Category) (c : Category),
+  λ a b c,
     a
 placeholder has type
   Category
diff --git a/tests/lean/errors.lean.expected.out b/tests/lean/errors.lean.expected.out
index 0b71c1332..9fb17498a 100644
--- a/tests/lean/errors.lean.expected.out
+++ b/tests/lean/errors.lean.expected.out
@@ -5,4 +5,4 @@ errors.lean:22:12: error: unknown identifier 'b'
 tst3 : A → A → A
 foo.tst1 : ℕ → ℕ → ℕ
 foo.tst2 : ℕ → ℕ → ℕ
-foo.tst3 : Π (A : Type), A → A → A
+foo.tst3 : Π A, A → A → A
diff --git a/tests/lean/eta_bug.lean.expected.out b/tests/lean/eta_bug.lean.expected.out
index 6ce8ac64d..9f1699359 100644
--- a/tests/lean/eta_bug.lean.expected.out
+++ b/tests/lean/eta_bug.lean.expected.out
@@ -1 +1 @@
-λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.rec H₁ H₂
+λ A x y H₁ H₂, eq.rec H₁ H₂
diff --git a/tests/lean/eta_decls.lean.expected.out b/tests/lean/eta_decls.lean.expected.out
index c7a7ad6dc..6106ac0eb 100644
--- a/tests/lean/eta_decls.lean.expected.out
+++ b/tests/lean/eta_decls.lean.expected.out
@@ -1,4 +1,2 @@
-to_set_union :
-  ∀ {A : Type} [deceq : decidable_eq A] (s t : finset A),
-    @eq (set A) (@ts A (@union A deceq s t)) (@set.union A (@ts A s) (@ts A t))
-to_set_empty : ∀ {A : Type}, @eq (set A) (@ts A (@empty A)) (@set.empty A)
+to_set_union : ∀ {A} [deceq] s t, @eq (set A) (@ts A (@union A deceq s t)) (@set.union A (@ts A s) (@ts A t))
+to_set_empty : ∀ {A}, @eq (set A) (@ts A (@empty A)) (@set.empty A)
diff --git a/tests/lean/extra/755.expected.out b/tests/lean/extra/755.expected.out
index 253f7dea6..d4c58cdef 100644
--- a/tests/lean/extra/755.expected.out
+++ b/tests/lean/extra/755.expected.out
@@ -3,6 +3,6 @@ position 55:52
 A : Type,
 B : Type,
 f : one_step_tr A → B
-⊢ Π (x y : A),
+⊢ Π x y,
     f (tr x) = f (tr y)
 END_LEAN_INFORMATION
diff --git a/tests/lean/extra/bag.671.8.expected.out b/tests/lean/extra/bag.671.8.expected.out
index dd8f84e03..ab0e67f8f 100644
--- a/tests/lean/extra/bag.671.8.expected.out
+++ b/tests/lean/extra/bag.671.8.expected.out
@@ -2,9 +2,7 @@ LEAN_INFORMATION
 position 671:8
 A : Type,
 decA : decidable_eq A,
-ex_of_subcount_eq_ff :
-  ∀ {l₁ l₂ : list A},
-    subcount l₁ l₂ = ff → (∃ (a : A), ¬list.count a l₁ ≤ list.count a l₂),
+ex_of_subcount_eq_ff : ∀ {l₁ l₂}, subcount l₁ l₂ = ff → (∃ a, ¬list.count a l₁ ≤ list.count a l₂),
 a : A,
 l₁ l₂ : list A,
 h : subcount (a :: l₁) l₂ = ff,
diff --git a/tests/lean/extra/bag.677.47.expected.out b/tests/lean/extra/bag.677.47.expected.out
index d9c83254a..79637bc78 100644
--- a/tests/lean/extra/bag.677.47.expected.out
+++ b/tests/lean/extra/bag.677.47.expected.out
@@ -2,15 +2,13 @@ LEAN_INFORMATION
 position 677:47
 A : Type,
 decA : decidable_eq A,
-ex_of_subcount_eq_ff :
-  ∀ {l₁ l₂ : list A},
-    subcount l₁ l₂ = ff → (∃ (a : A), ¬list.count a l₁ ≤ list.count a l₂),
+ex_of_subcount_eq_ff : ∀ {l₁ l₂}, subcount l₁ l₂ = ff → (∃ a, ¬list.count a l₁ ≤ list.count a l₂),
 a : A,
 l₁ l₂ : list A,
 h : subcount (a :: l₁) l₂ = ff,
 i : list.count a (a :: l₁) ≤ list.count a l₂,
 this : subcount l₁ l₂ = ff,
-ih : ∃ (a : A), ¬list.count a l₁ ≤ list.count a l₂,
+ih : ∃ a, ¬list.count a l₁ ≤ list.count a l₂,
 hw : ¬list.count a l₁ ≤ list.count a l₂
 ⊢ ¬list.count a (a :: l₁) ≤ list.count a l₂
 END_LEAN_INFORMATION
diff --git a/tests/lean/finset_induction_bug.lean.expected.out b/tests/lean/finset_induction_bug.lean.expected.out
index 978fe4b99..12bd5c556 100644
--- a/tests/lean/finset_induction_bug.lean.expected.out
+++ b/tests/lean/finset_induction_bug.lean.expected.out
@@ -13,23 +13,23 @@ A : Type,
 h : decidable_eq A,
 P : finset A → Prop,
 H1 : P (@empty A),
-H2 : ∀ ⦃s : finset A⦄ {a : A}, not (@mem A a s) → P s → P (@insert A h a s),
+H2 : ∀ ⦃s⦄ {a}, not (@mem A a s) → P s → P (@insert A h a s),
 s : finset A,
 u : nodup_list A,
 l : list A,
 a : A,
 l' : list A,
 IH :
-  ∀ (has_property : @nodup A l'),
+  ∀ has_property,
     P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' has_property)),
 nodup_al' : @nodup A (@cons A a l'),
 anl' : not (@list.mem A a l'),
-H3 : @eq (list A) (@list.insert A (λ (a b : A), h a b) a l') (@cons A a l'),
+H3 : @eq (list A) (@list.insert A (λ a b, h a b) a l') (@cons A a l'),
 nodup_l' : @nodup A l',
 P_l' : P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')),
 H4 :
   P
-    (@insert A (λ (a b : A), h a b) a
+    (@insert A (λ a b, h a b) a
        (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')))
 ⊢ P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) (@cons A a l') nodup_al'))
 finset_induction_bug.lean:30:45: error: don't know how to synthesize placeholder
@@ -37,34 +37,34 @@ A : Type,
 h : decidable_eq A,
 P : finset A → Prop,
 H1 : P (@empty A),
-H2 : ∀ ⦃s : finset A⦄ {a : A}, not (@mem A a s) → P s → P (@insert A h a s),
+H2 : ∀ ⦃s⦄ {a}, not (@mem A a s) → P s → P (@insert A h a s),
 s : finset A,
 u : nodup_list A,
 l : list A,
 a : A,
 l' : list A,
 IH :
-  ∀ (has_property : @nodup A l'),
+  ∀ has_property,
     P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' has_property)),
 nodup_al' : @nodup A (@cons A a l'),
 anl' : not (@list.mem A a l'),
-H3 : @eq (list A) (@list.insert A (λ (a b : A), h a b) a l') (@cons A a l'),
+H3 : @eq (list A) (@list.insert A (λ a b, h a b) a l') (@cons A a l'),
 nodup_l' : @nodup A l',
 P_l' : P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')),
 H4 :
   P
-    (@insert A (λ (a b : A), h a b) a
+    (@insert A (λ a b, h a b) a
        (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')))
 ⊢ P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) (@cons A a l') nodup_al'))
 finset_induction_bug.lean:16:5: error: failed to add declaration 'finset.induction₂' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (h : …) (P : …) (H1 : …) (H2 : …) (s : …),
+  λ A h P H1 H2 s,
     @quot.induction_on … … P s
-      (λ (u : …),
+      (λ u,
          @subtype.destruct … … … u
-           (λ (l : …),
+           (λ l,
               @list.induction_on A … l …
-                (λ (a : A) (l' : …) (IH : …) (nodup_al' : …),
+                (λ a l' IH nodup_al',
                    have anl' : …, from …,
                    have H3 : …, from …,
                    have nodup_l' : …, from …,
diff --git a/tests/lean/gen_as.lean.expected.out b/tests/lean/gen_as.lean.expected.out
index 7be3850cf..6ec1c90d2 100644
--- a/tests/lean/gen_as.lean.expected.out
+++ b/tests/lean/gen_as.lean.expected.out
@@ -1,4 +1,4 @@
 gen_as.lean:7:2: proof state
 x y : ℕ
-⊢ ∀ (n : ℕ),
+⊢ ∀ n,
     n ≥ 0
diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out
index f1ca174f2..442440e2a 100644
--- a/tests/lean/interactive/alias.input.expected.out
+++ b/tests/lean/interactive/alias.input.expected.out
@@ -5,42 +5,42 @@
 -- BEGINFINDP
 bool.tt_bxor_tt|eq (bool.bxor bool.tt bool.tt) bool.ff
 bool.tt_bxor_ff|eq (bool.bxor bool.tt bool.ff) bool.tt
-bool.bor_tt|∀ (a : bool), eq (bool.bor a bool.tt) bool.tt
-bool.band_tt|∀ (a : bool), eq (bool.band a bool.tt) a
+bool.bor_tt|∀ a, eq (bool.bor a bool.tt) bool.tt
+bool.band_tt|∀ a, eq (bool.band a bool.tt) a
 bool.tt|bool
-bool.bxor_tt|∀ (a : bool), eq (bool.bxor a bool.tt) (bool.bnot a)
+bool.bxor_tt|∀ a, eq (bool.bxor a bool.tt) (bool.bnot a)
 bool.eq_tt_of_bnot_eq_ff|eq (bool.bnot ?a) bool.ff → eq ?a bool.tt
 bool.eq_ff_of_bnot_eq_tt|eq (bool.bnot ?a) bool.tt → eq ?a bool.ff
 bool.ff_bxor_tt|eq (bool.bxor bool.ff bool.tt) bool.tt
 bool.absurd_of_eq_ff_of_eq_tt|eq ?a bool.ff → eq ?a bool.tt → ?B
 bool.eq_tt_of_ne_ff|ne ?a bool.ff → eq ?a bool.tt
 tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic
-bool.tt_band|∀ (a : bool), eq (bool.band bool.tt a) a
-bool.cond_tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t
+bool.tt_band|∀ a, eq (bool.band bool.tt a) a
+bool.cond_tt|∀ t e, eq (bool.cond bool.tt t e) t
 bool.ff_ne_tt|eq bool.ff bool.tt → false
 bool.eq_ff_of_ne_tt|ne ?a bool.tt → eq ?a bool.ff
-bool.tt_bxor|∀ (a : bool), eq (bool.bxor bool.tt a) (bool.bnot a)
-bool.tt_bor|∀ (a : bool), eq (bool.bor bool.tt a) bool.tt
+bool.tt_bxor|∀ a, eq (bool.bxor bool.tt a) (bool.bnot a)
+bool.tt_bor|∀ a, eq (bool.bor bool.tt a) bool.tt
 -- ENDFINDP
 -- BEGINWAIT
 -- ENDWAIT
 -- BEGINFINDP
 tt|bool
-tt_bor|∀ (a : bool), eq (bor tt a) tt
-tt_band|∀ (a : bool), eq (band tt a) a
-tt_bxor|∀ (a : bool), eq (bxor tt a) (bnot a)
+tt_bor|∀ a, eq (bor tt a) tt
+tt_band|∀ a, eq (band tt a) a
+tt_bxor|∀ a, eq (bxor tt a) (bnot a)
 tt_bxor_tt|eq (bxor tt tt) ff
 tt_bxor_ff|eq (bxor tt ff) tt
-bor_tt|∀ (a : bool), eq (bor a tt) tt
-band_tt|∀ (a : bool), eq (band a tt) a
-bxor_tt|∀ (a : bool), eq (bxor a tt) (bnot a)
+bor_tt|∀ a, eq (bor a tt) tt
+band_tt|∀ a, eq (band a tt) a
+bxor_tt|∀ a, eq (bxor a tt) (bnot a)
 eq_tt_of_bnot_eq_ff|eq (bnot ?a) ff → eq ?a tt
 eq_ff_of_bnot_eq_tt|eq (bnot ?a) tt → eq ?a ff
 ff_bxor_tt|eq (bxor ff tt) tt
 absurd_of_eq_ff_of_eq_tt|eq ?a ff → eq ?a tt → ?B
 eq_tt_of_ne_ff|ne ?a ff → eq ?a tt
 tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic
-cond_tt|∀ (t e : ?A), eq (cond tt t e) t
+cond_tt|∀ t e, eq (cond tt t e) t
 ff_ne_tt|eq ff tt → false
 eq_ff_of_ne_tt|ne ?a tt → eq ?a ff
 -- ENDFINDP
diff --git a/tests/lean/interactive/auto_comp.input.expected.out b/tests/lean/interactive/auto_comp.input.expected.out
index 40c3370a0..eb6105e25 100644
--- a/tests/lean/interactive/auto_comp.input.expected.out
+++ b/tests/lean/interactive/auto_comp.input.expected.out
@@ -1,12 +1,12 @@
 -- BEGINWAIT
 -- ENDWAIT
 -- BEGINFINDP
-le.rec_on|le ?a ?a → (Π (a : nat), ?C a a) → ?C ?a ?a
-nat.rec_on|Π (n : nat), ?C 0 → (Π (a : nat), ?C a → ?C (succ a)) → ?C n
-bool.rec_on|Π (n : bool), ?C bool.ff → ?C bool.tt → ?C n
+le.rec_on|le ?a ?a → (Π a, ?C a a) → ?C ?a ?a
+nat.rec_on|Π n, ?C 0 → (Π a, ?C a → ?C (succ a)) → ?C n
+bool.rec_on|Π n, ?C bool.ff → ?C bool.tt → ?C n
 -- ENDFINDP
 -- BEGINFINDP
-nat.le.rec_on|nat.le ?a ?a → (Π (a : nat), ?C a a) → ?C ?a ?a
-nat.rec_on|Π (n : nat), ?C 0 → (Π (a : nat), ?C a → ?C (nat.succ a)) → ?C n
-bool.rec_on|Π (n : bool), ?C bool.ff → ?C bool.tt → ?C n
+nat.le.rec_on|nat.le ?a ?a → (Π a, ?C a a) → ?C ?a ?a
+nat.rec_on|Π n, ?C 0 → (Π a, ?C a → ?C (nat.succ a)) → ?C n
+bool.rec_on|Π n, ?C bool.ff → ?C bool.tt → ?C n
 -- ENDFINDP
diff --git a/tests/lean/interactive/consume_args.input.expected.out b/tests/lean/interactive/consume_args.input.expected.out
index 8bb7be876..4db48fc66 100644
--- a/tests/lean/interactive/consume_args.input.expected.out
+++ b/tests/lean/interactive/consume_args.input.expected.out
@@ -41,7 +41,7 @@ by
 rewrite
 -- ACK
 -- TYPE|7|42
-∀ (a_1 b_1 c_1 : ?A), (:a_1 + b_1 + c_1:) = (:a_1 + (b_1 + c_1):)
+∀ a_1 b_1 c_1, (:a_1 + b_1 + c_1:) = (:a_1 + (b_1 + c_1):)
 -- ACK
 -- IDENTIFIER|7|42
 add.assoc
diff --git a/tests/lean/interactive/eq2.input.expected.out b/tests/lean/interactive/eq2.input.expected.out
index ac65316f5..eb25f20ab 100644
--- a/tests/lean/interactive/eq2.input.expected.out
+++ b/tests/lean/interactive/eq2.input.expected.out
@@ -51,7 +51,7 @@ b₂
 c₂
 -- ACK
 -- TYPE|134|38
-Π (a : A), B a → Type
+Π a, B a → Type
 -- ACK
 -- IDENTIFIER|134|38
 C
diff --git a/tests/lean/interactive/mod.input.expected.out b/tests/lean/interactive/mod.input.expected.out
index 66c926654..257d479c1 100644
--- a/tests/lean/interactive/mod.input.expected.out
+++ b/tests/lean/interactive/mod.input.expected.out
@@ -3,18 +3,18 @@
 -- BEGINWAIT
 -- ENDWAIT
 -- BEGINEVAL
-my_id : Π {A : Type}, A → A
+my_id : Π {A}, A → A
 -- ENDEVAL
 -- BEGINEVAL
-my_id2 : Π {A : Type}, A → A
+my_id2 : Π {A}, A → A
 -- ENDEVAL
 -- BEGINSAVE
 -- ENDSAVE
 -- BEGINWAIT
 -- ENDWAIT
 -- BEGINEVAL
-my_id : Π {A : Type}, A → A
+my_id : Π {A}, A → A
 -- ENDEVAL
 -- BEGINEVAL
-my_id2 : Π {A : Type}, A → A
+my_id2 : Π {A}, A → A
 -- ENDEVAL
diff --git a/tests/lean/interactive/num2.input.expected.out b/tests/lean/interactive/num2.input.expected.out
index 233b2524a..3e86e436d 100644
--- a/tests/lean/interactive/num2.input.expected.out
+++ b/tests/lean/interactive/num2.input.expected.out
@@ -9,23 +9,23 @@ pos_num.is_inhabited|inhabited pos_num
 pos_num.is_one|pos_num → bool
 pos_num.inc|pos_num → pos_num
 pos_num.ibelow|pos_num → Prop
-pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
-pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.binduction_on|Π n, (Π n, pos_num.ibelow n → ?C n) → ?C n
+pos_num.induction_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num.succ|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
-pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
+pos_num.rec|?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → (Π n, ?C n)
 pos_num.one|pos_num
 pos_num.below|pos_num → Type
 pos_num.le|pos_num → pos_num → bool
-pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n
+pos_num.cases_on|Π n, ?C pos_num.one → (Π a, ?C (pos_num.bit1 a)) → (Π a, ?C (pos_num.bit0 a)) → ?C n
 pos_num.pred|pos_num → pos_num
 pos_num.mul|pos_num → pos_num → pos_num
 pos_num.no_confusion_type|Type → pos_num → pos_num → Type
 pos_num.num_bits|pos_num → pos_num
 pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
 pos_num.lt|pos_num → pos_num → bool
-pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
-pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n
+pos_num.rec_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.brec_on|Π n, (Π n, pos_num.below n → ?C n) → ?C n
 pos_num.add|pos_num → pos_num → pos_num
 pos_num_has_mul|has_mul pos_num
 pos_num|Type
@@ -43,22 +43,22 @@ pos_num.is_inhabited|inhabited pos_num
 pos_num.is_one|pos_num → bool
 pos_num.inc|pos_num → pos_num
 pos_num.ibelow|pos_num → Prop
-pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
-pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.binduction_on|Π n, (Π n, pos_num.ibelow n → ?C n) → ?C n
+pos_num.induction_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num.succ|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
-pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
+pos_num.rec|?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → (Π n, ?C n)
 pos_num.one|pos_num
 pos_num.below|pos_num → Type
 pos_num.le|pos_num → pos_num → bool
-pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n
+pos_num.cases_on|Π n, ?C pos_num.one → (Π a, ?C (pos_num.bit1 a)) → (Π a, ?C (pos_num.bit0 a)) → ?C n
 pos_num.pred|pos_num → pos_num
 pos_num.mul|pos_num → pos_num → pos_num
 pos_num.no_confusion_type|Type → pos_num → pos_num → Type
 pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
 pos_num.lt|pos_num → pos_num → bool
-pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
-pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n
+pos_num.rec_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.brec_on|Π n, (Π n, pos_num.below n → ?C n) → ?C n
 pos_num.add|pos_num → pos_num → pos_num
 pos_num_has_mul|has_mul pos_num
 pos_num|Type
@@ -72,22 +72,22 @@ pos_num.is_inhabited|inhabited pos_num
 pos_num.is_one|pos_num → bool
 pos_num.inc|pos_num → pos_num
 pos_num.ibelow|pos_num → Prop
-pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
-pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.binduction_on|Π n, (Π n, pos_num.ibelow n → ?C n) → ?C n
+pos_num.induction_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num.succ|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
-pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
+pos_num.rec|?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → (Π n, ?C n)
 pos_num.one|pos_num
 pos_num.below|pos_num → Type
 pos_num.le|pos_num → pos_num → bool
-pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n
+pos_num.cases_on|Π n, ?C pos_num.one → (Π a, ?C (pos_num.bit1 a)) → (Π a, ?C (pos_num.bit0 a)) → ?C n
 pos_num.pred|pos_num → pos_num
 pos_num.mul|pos_num → pos_num → pos_num
 pos_num.no_confusion_type|Type → pos_num → pos_num → Type
 pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
 pos_num.lt|pos_num → pos_num → bool
-pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
-pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n
+pos_num.rec_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.brec_on|Π n, (Π n, pos_num.below n → ?C n) → ?C n
 pos_num.add|pos_num → pos_num → pos_num
 pos_num_has_mul|has_mul pos_num
 pos_num|Type
diff --git a/tests/lean/interactive/proof_qed.input.expected.out b/tests/lean/interactive/proof_qed.input.expected.out
index fd84ef4f9..9541392e1 100644
--- a/tests/lean/interactive/proof_qed.input.expected.out
+++ b/tests/lean/interactive/proof_qed.input.expected.out
@@ -5,7 +5,7 @@
 @
 -- ACK
 -- TYPE|11|5
-∀ {A : Type} {a b c : A}, eq a b → eq b c → eq a c
+∀ {A} {a b c}, eq a b → eq b c → eq a c
 -- ACK
 -- IDENTIFIER|11|5
 eq.trans
diff --git a/tests/lean/inv_del.lean.expected.out b/tests/lean/inv_del.lean.expected.out
index de25fcf6b..f46c7fc86 100644
--- a/tests/lean/inv_del.lean.expected.out
+++ b/tests/lean/inv_del.lean.expected.out
@@ -1,7 +1,7 @@
 inv_del.lean:15:2: error: 1 unsolved subgoal
 A : Type,
 P : vec A 1 → Type,
-H : Π (a : A), P (vone a),
+H : Π a, P (vone a),
 a : A
 ⊢ P (vone a)
 inv_del.lean:15:2: error: failed to add declaration 'vec.eone' to environment, value has metavariables
diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out
index fac71d250..10554547f 100644
--- a/tests/lean/let1.lean.expected.out
+++ b/tests/lean/let1.lean.expected.out
@@ -1,15 +1,15 @@
 let bool := Prop,
-    and := λ (p q : bool), Π (c : bool), (p → q → c) → c,
-    and_intro := λ (p q : bool) (H1 : p) (H2 : q) (c : bool) (H : p → q → c), H H1 H2
+    and := λ p q, Π c, (p → q → c) → c,
+    and_intro := λ p q H1 H2 c H, H H1 H2
 in and_intro :
-  ∀ (p q : Prop),
-    p → q → (∀ (c : Prop), (p → q → c) → c)
+  ∀ p q,
+    p → q → (∀ c, (p → q → c) → c)
 let1.lean:19:19: error: type mismatch at term
-  λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
+  λ p q H1 H2 c H,
     H H1 H2
 has type
-  ∀ (p q : Prop),
-    p → q → (∀ (c : Prop), (p → q → c) → c)
+  ∀ p q,
+    p → q → (∀ c, (p → q → c) → c)
 but is expected to have type
-  ∀ (p q : Prop),
-    p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p
+  ∀ p q,
+    p → q → (λ p q, ∀ c, (p → q → c) → c) q p
diff --git a/tests/lean/nested1.lean.expected.out b/tests/lean/nested1.lean.expected.out
index d2c80028c..e40bf5b2c 100644
--- a/tests/lean/nested1.lean.expected.out
+++ b/tests/lean/nested1.lean.expected.out
@@ -1,8 +1,8 @@
 definition test.foo.prf [irreducible] : ∀ (x : ℕ), 0 < succ (succ x) :=
-λ (x : ℕ), lt.step (zero_lt_succ x)
+λ x, lt.step (zero_lt_succ x)
 definition test.bla : ℕ → ℕ :=
-λ (a : ℕ), foo (succ (succ a)) (foo.prf a)
+λ a, foo (succ (succ a)) (foo.prf a)
 definition test.bla : ℕ → ℕ :=
-λ (a : ℕ), test.foo (succ (succ a)) (test.foo.prf a)
+λ a, test.foo (succ (succ a)) (test.foo.prf a)
 definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x) :=
-λ (x : ℕ), lt.step (zero_lt_succ x)
+λ x, lt.step (zero_lt_succ x)
diff --git a/tests/lean/nested2.lean.expected.out b/tests/lean/nested2.lean.expected.out
index 464debfc1..78d09e913 100644
--- a/tests/lean/nested2.lean.expected.out
+++ b/tests/lean/nested2.lean.expected.out
@@ -1,15 +1,15 @@
 definition bla : ℕ → ℕ :=
-λ (a : ℕ), foo (succ (succ a)) (bla_2 a)
+λ a, foo (succ (succ a)) (bla_2 a)
 definition bla_1 : ∀ (x : ℕ), 0 < succ x :=
-λ (x : ℕ), zero_lt_succ x
+λ x, zero_lt_succ x
 definition bla_2 : ∀ (x : ℕ), 0 < succ (succ x) :=
-λ (x : ℕ), lt.step (bla_1 x)
+λ x, lt.step (bla_1 x)
 definition test_1 [irreducible] : ∀ (x : ℕ), 0 < succ x :=
-λ (x : ℕ), zero_lt_succ x
+λ x, zero_lt_succ x
 definition test_2 [reducible] : ∀ (x : ℕ), 0 < succ (succ x) :=
-λ (x : ℕ), lt.step (test_1 x)
+λ x, lt.step (test_1 x)
 definition tst_1 : ∀ (x : Type.{l_1}) (x_1 : x) (x_2 : list.{l_1} x),
   x_1 :: x_2 = nil.{l_1} → list.no_confusion_type.{0 l_1} false (x_1 :: x_2) nil.{l_1} :=
-λ (x : Type.{l_1}) (x_1 : x) (x_2 : list.{l_1} x), list.no_confusion.{0 l_1}
+λ x x_1 x_2, list.no_confusion.{0 l_1}
 definition tst : Π {A : Type.{l_1}}, A → list.{l_1} A → bool :=
-λ (A : Type.{l_1}) (a : A) (l : list.{l_1} A), voo.{(max 1 l_1)} (a :: l) nil.{l_1} (tst_1.{l_1} A a l)
+λ A a l, voo.{(max 1 l_1)} (a :: l) nil.{l_1} (tst_1.{l_1} A a l)
diff --git a/tests/lean/noncomp_theory.lean.expected.out b/tests/lean/noncomp_theory.lean.expected.out
index dfa6026e4..871c175b0 100644
--- a/tests/lean/noncomp_theory.lean.expected.out
+++ b/tests/lean/noncomp_theory.lean.expected.out
@@ -1,5 +1,5 @@
 noncomp_theory.lean:4:0: error: definition 'f' is noncomputable, it depends on 'real.discrete_linear_ordered_field'
 noncomputable definition g : ℝ → ℝ → ℝ :=
-λ (a : ℝ), div (a + a)
+λ a, div (a + a)
 definition r : ℕ → ℕ :=
-λ (a : ℕ), a
+λ a, a
diff --git a/tests/lean/notation4.lean.expected.out b/tests/lean/notation4.lean.expected.out
index d5a812e95..9a28e86a5 100644
--- a/tests/lean/notation4.lean.expected.out
+++ b/tests/lean/notation4.lean.expected.out
@@ -1,4 +1,4 @@
-∃ (A : Type₁) (x y : A), x = y : Prop
-∃ (x : num), x = 0 : Prop
-Σ (x : num), x = 10 : Type₁
-Σ (A : Type₁), list A : Type₂
+∃ A x y, x = y : Prop
+∃ x, x = 0 : Prop
+Σ x, x = 10 : Type₁
+Σ A, list A : Type₂
diff --git a/tests/lean/omit.lean.expected.out b/tests/lean/omit.lean.expected.out
index c85494d57..d16188f6a 100644
--- a/tests/lean/omit.lean.expected.out
+++ b/tests/lean/omit.lean.expected.out
@@ -1,4 +1,4 @@
 omit.lean:5:7: error: invalid omit command, 'A' has not been included
 omit.lean:7:10: error: invalid include command, 'A' has already been included
-foo : Π (A : Type), A → A → (Π (B : Type), B → B)
-tst : Π (A : Type), A → A → Type → Type
+foo : Π A, A → A → (Π B, B → B)
+tst : Π A, A → A → Type → Type
diff --git a/tests/lean/param_binder_update.lean.expected.out b/tests/lean/param_binder_update.lean.expected.out
index 0e1e63115..277f9f497 100644
--- a/tests/lean/param_binder_update.lean.expected.out
+++ b/tests/lean/param_binder_update.lean.expected.out
@@ -1,17 +1,17 @@
-id : Π {A : Type}, A → A
-id₂ : Π {A : Type}, A → A
+id : Π {A}, A → A
+id₂ : Π {A}, A → A
 foo1 : A → B → A
 foo2 : A → B → A
 foo3 : A → B → A
 foo4 : A → B → A
-foo1 : Π {A : Type} {B : Type}, A → B → A
-foo2 : Π {A : Type} (B : Type), A → B → A
-foo3 : Π (A : Type) {B : Type}, A → B → A
-foo4 : Π (A : Type) (B : Type), A → B → A
-boo1 : Π {A : Type} {B : Type}, A → B → A
-boo2 : Π {A : Type} (B : Type), A → B → A
-boo3 : Π (A : Type) {B : Type}, A → B → A
-boo4 : Π (A : Type) (B : Type), A → B → A
+foo1 : Π {A} {B}, A → B → A
+foo2 : Π {A} B, A → B → A
+foo3 : Π A {B}, A → B → A
+foo4 : Π A B, A → B → A
+boo1 : Π {A} {B}, A → B → A
+boo2 : Π {A} B, A → B → A
+boo3 : Π A {B}, A → B → A
+boo4 : Π A B, A → B → A
 param_binder_update.lean:70:12: error: invalid parameter binder type update, 'A' is a variable
 param_binder_update.lean:71:11: error: invalid variable binder type update, 'C' is not a variable
 param_binder_update.lean:72:12: error: invalid variable binder type update, 'C' is not a variable
diff --git a/tests/lean/param_binder_update2.lean.expected.out b/tests/lean/param_binder_update2.lean.expected.out
index b5b750ee7..93052f069 100644
--- a/tests/lean/param_binder_update2.lean.expected.out
+++ b/tests/lean/param_binder_update2.lean.expected.out
@@ -1,4 +1,4 @@
-foo1 : Π {A : Type} {B : Type}, A → B → A
-foo2 : Π {A : Type} (B : Type), A → B → A
-foo3 : Π (A : Type) {B : Type}, A → B → A
-foo4 : Π (A : Type) (B : Type), A → B → A
+foo1 : Π {A} {B}, A → B → A
+foo2 : Π {A} B, A → B → A
+foo3 : Π A {B}, A → B → A
+foo4 : Π A B, A → B → A
diff --git a/tests/lean/pattern_pp.lean.expected.out b/tests/lean/pattern_pp.lean.expected.out
index 9297527d7..038e0067a 100644
--- a/tests/lean/pattern_pp.lean.expected.out
+++ b/tests/lean/pattern_pp.lean.expected.out
@@ -1,5 +1,5 @@
 definition Sum_weird [forward] : ∀ (f g h : ℕ → ℕ) (n : ℕ), Sum n (λ (x : ℕ), f (g (h x))) = 1 :=
-λ (f g h : ℕ → ℕ) (n : ℕ), sorry
+λ f g h n, sorry
 (multi-)patterns:
 ?M_1 : ℕ → ℕ, ?M_2 : ℕ → ℕ, ?M_3 : ℕ → ℕ, ?M_4 : ℕ
-{Sum ?M_4 (λ (x : ℕ), ?M_1 (?M_2 (?M_3 x)))}
+{Sum ?M_4 (λ x, ?M_1 (?M_2 (?M_3 x)))}
diff --git a/tests/lean/pp.lean.expected.out b/tests/lean/pp.lean.expected.out
index 62e780e88..b7ff9cacd 100644
--- a/tests/lean/pp.lean.expected.out
+++ b/tests/lean/pp.lean.expected.out
@@ -1,7 +1,7 @@
-λ {A : Type} (B : Type) (a : A) (b : B), a : Π (B : Type), ?A → B → ?A
-λ {A B : Type} (a : A) (b : B), a : ?A → ?B → ?A
-λ (A : Type) {B : Type} (a : A) (b : B), a : Π (A : Type) {B : Type}, A → B → A
-λ (A B : Type) (a : A) (b : B), a : Π (A B : Type), A → B → A
-λ [A : Type] (B : Type) (a : A) (b : B), a : Π (B : Type), ?A → B → ?A
-λ ⦃A : Type⦄ {B : Type} (a : A) (b : B), a : Π ⦃A : Type⦄ {B : Type}, A → B → A
-λ ⦃A B : Type⦄ (a : A) (b : B), a : Π ⦃A B : Type⦄, A → B → A
+λ {A} B a b, a : Π B, ?A → B → ?A
+λ {A B} a b, a : ?A → ?B → ?A
+λ A {B} a b, a : Π A {B}, A → B → A
+λ A B a b, a : Π A B, A → B → A
+λ [A] B a b, a : Π B, ?A → B → ?A
+λ ⦃A⦄ {B} a b, a : Π ⦃A⦄ {B}, A → B → A
+λ ⦃A B⦄ a b, a : Π ⦃A B⦄, A → B → A
diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out
index d40a12b76..bab4e59b6 100644
--- a/tests/lean/pp_all.lean.expected.out
+++ b/tests/lean/pp_all.lean.expected.out
@@ -1,6 +1,6 @@
 a + of_num b = 10 : Prop
 @eq.{1} nat
-  (@add.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 ((λ (x : nat), x) a)
+  (@add.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 ((λ x, x) a)
      (nat.of_num (@bit0.{1} num num_has_add (@one.{1} num num_has_one))))
   (@bit0.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2
      (@bit1.{1} nat nat._trans_of_decidable_linear_ordered_semiring_22 nat._trans_of_decidable_linear_ordered_semiring_2
diff --git a/tests/lean/pp_beta.lean.expected.out b/tests/lean/pp_beta.lean.expected.out
index e214e6af9..5232dcad3 100644
--- a/tests/lean/pp_beta.lean.expected.out
+++ b/tests/lean/pp_beta.lean.expected.out
@@ -1,2 +1,2 @@
 1 : ℕ
-(λ (x : ℕ), x) 1 : ℕ
+(λ x, x) 1 : ℕ
diff --git a/tests/lean/ppbug.lean.expected.out b/tests/lean/ppbug.lean.expected.out
index 69f152c42..dfa2a8091 100644
--- a/tests/lean/ppbug.lean.expected.out
+++ b/tests/lean/ppbug.lean.expected.out
@@ -1,3 +1 @@
-char.rec_on :
-  Π (n : char),
-    (Π (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : bool), ?C (char.mk a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → ?C n
+char.rec_on : Π n, (Π a a_1 a_2 a_3 a_4 a_5 a_6 a_7, ?C (char.mk a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → ?C n
diff --git a/tests/lean/print_ax1.lean.expected.out b/tests/lean/print_ax1.lean.expected.out
index fadf6bc0b..bee4bf38e 100644
--- a/tests/lean/print_ax1.lean.expected.out
+++ b/tests/lean/print_ax1.lean.expected.out
@@ -1,3 +1,3 @@
-quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
-classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A | Exists P → P x}
-propext : ∀ {a b : Prop}, (a ↔ b) → a = b
+quot.sound : ∀ {A} [s] {a b}, setoid.r a b → quot.mk a = quot.mk b
+classical.strong_indefinite_description : Π {A} P, nonempty A → {x | Exists P → P x}
+propext : ∀ {a b}, (a ↔ b) → a = b
diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out
index fadf6bc0b..bee4bf38e 100644
--- a/tests/lean/print_ax2.lean.expected.out
+++ b/tests/lean/print_ax2.lean.expected.out
@@ -1,3 +1,3 @@
-quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
-classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A | Exists P → P x}
-propext : ∀ {a b : Prop}, (a ↔ b) → a = b
+quot.sound : ∀ {A} [s] {a b}, setoid.r a b → quot.mk a = quot.mk b
+classical.strong_indefinite_description : Π {A} P, nonempty A → {x | Exists P → P x}
+propext : ∀ {a b}, (a ↔ b) → a = b
diff --git a/tests/lean/print_ax3.lean.expected.out b/tests/lean/print_ax3.lean.expected.out
index c2a45fd30..e70648cda 100644
--- a/tests/lean/print_ax3.lean.expected.out
+++ b/tests/lean/print_ax3.lean.expected.out
@@ -1,8 +1,8 @@
 no axioms
 ------
-quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
-classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A | Exists P → P x}
-propext : ∀ {a b : Prop}, (a ↔ b) → a = b
+quot.sound : ∀ {A} [s] {a b}, setoid.r a b → quot.mk a = quot.mk b
+classical.strong_indefinite_description : Π {A} P, nonempty A → {x | Exists P → P x}
+propext : ∀ {a b}, (a ↔ b) → a = b
 ------
 theorem foo3 : 0 = 0 :=
 foo2
diff --git a/tests/lean/protected_test.lean.expected.out b/tests/lean/protected_test.lean.expected.out
index 86174bc94..68342737a 100644
--- a/tests/lean/protected_test.lean.expected.out
+++ b/tests/lean/protected_test.lean.expected.out
@@ -1,7 +1,7 @@
 protected_test.lean:2:8: error: unknown identifier 'induction_on'
 protected_test.lean:3:8: error: unknown identifier 'rec_on'
-nat.induction_on : ∀ (n : ℕ), ?C 0 → (∀ (a : ℕ), ?C a → ?C (succ a)) → ?C n
-le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b : ℕ}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1
-le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b : ℕ}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1
+nat.induction_on : ∀ n, ?C 0 → (∀ a, ?C a → ?C (succ a)) → ?C n
+le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1
+le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1
 protected_test.lean:8:10: error: unknown identifier 'rec_on'
-le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b : ℕ}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1
+le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1
diff --git a/tests/lean/pstate.lean.expected.out b/tests/lean/pstate.lean.expected.out
index 7253037ab..84308574a 100644
--- a/tests/lean/pstate.lean.expected.out
+++ b/tests/lean/pstate.lean.expected.out
@@ -6,5 +6,5 @@ h₂ : b = c
 ⊢ b = c
 pstate.lean:4:7: error: failed to add declaration 'foo' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (a b c : A) (h₁ : …) (h₂ : …),
+  λ A a b c h₁ h₂,
     eq.trans h₁ ?M_1
diff --git a/tests/lean/quot_bug.lean.expected.out b/tests/lean/quot_bug.lean.expected.out
index d925317ac..4f1484d92 100644
--- a/tests/lean/quot_bug.lean.expected.out
+++ b/tests/lean/quot_bug.lean.expected.out
@@ -1 +1 @@
-λ (x : A), f x
+λ x, f x
diff --git a/tests/lean/redundant_pattern.lean.expected.out b/tests/lean/redundant_pattern.lean.expected.out
index 535233e15..69816b6bf 100644
--- a/tests/lean/redundant_pattern.lean.expected.out
+++ b/tests/lean/redundant_pattern.lean.expected.out
@@ -1,5 +1,5 @@
 definition foo [forward] : ∀ (m n k : ℕ), P (f m) → P (g n) → P (f k) → P k ∧ R (g m) (f n) ∧ P (g m) ∧ P (f n) :=
-λ (m n k : ℕ), sorry
+λ m n k, sorry
 (multi-)patterns:
 ?M_1 : ℕ, ?M_2 : ℕ, ?M_3 : ℕ
 {P ?M_3, R (g ?M_1) (f ?M_2)}
diff --git a/tests/lean/replace_tac.lean.expected.out b/tests/lean/replace_tac.lean.expected.out
index 0a4279f34..9cdb7e93c 100644
--- a/tests/lean/replace_tac.lean.expected.out
+++ b/tests/lean/replace_tac.lean.expected.out
@@ -32,4 +32,4 @@ replace_tac.lean:26:0: error: 1 unsolved subgoal
 ⊢ f 4 = p
 replace_tac.lean:26:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  ?M_1
\ No newline at end of file
+  ?M_1
diff --git a/tests/lean/sec_param_pp2.lean.expected.out b/tests/lean/sec_param_pp2.lean.expected.out
index 3d6831912..8c61bab16 100644
--- a/tests/lean/sec_param_pp2.lean.expected.out
+++ b/tests/lean/sec_param_pp2.lean.expected.out
@@ -1,4 +1,4 @@
 id2 : (A → B → A) → A
 id2 : (A → B → A) → A
 id2 : ?B a → (A → ?B a → A) → A
-id2 : ?A → (Π {B : Type}, B → (?A → B → ?A) → ?A)
+id2 : ?A → (Π {B}, B → (?A → B → ?A) → ?A)
diff --git a/tests/lean/show_tac.lean.expected.out b/tests/lean/show_tac.lean.expected.out
index a9b5fed35..2466af237 100644
--- a/tests/lean/show_tac.lean.expected.out
+++ b/tests/lean/show_tac.lean.expected.out
@@ -14,5 +14,5 @@ Hb : b
 ⊢ b ∧ a
 show_tac.lean:7:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b : Prop) (Hab : …),
+  λ a b Hab,
     ?M_1
diff --git a/tests/lean/simplifier2.lean.expected.out b/tests/lean/simplifier2.lean.expected.out
index c6e665817..d24fec2fd 100644
--- a/tests/lean/simplifier2.lean.expected.out
+++ b/tests/lean/simplifier2.lean.expected.out
@@ -1,2 +1,2 @@
-λ (a b c : bool), g y
-λ (a b c : bool), h z
+λ a b c, g y
+λ a b c, h z
diff --git a/tests/lean/simplifier6.lean.expected.out b/tests/lean/simplifier6.lean.expected.out
index 6cab9461e..fefbef4ac 100644
--- a/tests/lean/simplifier6.lean.expected.out
+++ b/tests/lean/simplifier6.lean.expected.out
@@ -1,4 +1,4 @@
 H1
 imp_congr H1 H2
 imp_congr H1 (imp_congr H2 H3)
-forall_congr (λ (x : T), H x)
+forall_congr (λ x, H x)
diff --git a/tests/lean/simplifier9.lean.expected.out b/tests/lean/simplifier9.lean.expected.out
index 28b9423df..9cd197ea7 100644
--- a/tests/lean/simplifier9.lean.expected.out
+++ b/tests/lean/simplifier9.lean.expected.out
@@ -1,14 +1,14 @@
 x = y → true
 T → x = y → true
-∀ (a : T), x = a → a = y
-∀ (a : T), a = x → true
+∀ a, x = a → a = y
+∀ a, a = x → true
 T → T → x = y → true
 T → T → x = y → P y
-(∀ (x : T), P x ↔ Q x) → Q x
-Prop → (∀ (x : T), P x ↔ Q x) → Prop → Q x
-∀ (a : Prop), (∀ (x : T), P x ↔ Q x) → a ∨ Q x
-(∀ (x : T), P x ↔ Q x) → Q x
-∀ (a : T), T → (∀ (x : T), P x ↔ Q x) → Q a
-∀ (a a_1 : T), a = a_1 → P a_1
-∀ (a a_1 a_2 : T), a = a_1 → a_1 = a_2 → P a_2
-∀ (a a_1 : T), a = a_1 → (∀ (w : T), P w ↔ Q w) → Q a_1
+(∀ x, P x ↔ Q x) → Q x
+Prop → (∀ x, P x ↔ Q x) → Prop → Q x
+∀ a, (∀ x, P x ↔ Q x) → a ∨ Q x
+(∀ x, P x ↔ Q x) → Q x
+∀ a, T → (∀ x, P x ↔ Q x) → Q a
+∀ a a_1, a = a_1 → P a_1
+∀ a a_1 a_2, a = a_1 → a_1 = a_2 → P a_2
+∀ a a_1, a = a_1 → (∀ w, P w ↔ Q w) → Q a_1
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index bf4b448aa..641ab5d1b 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/tests/lean/struct_class.lean.expected.out
@@ -17,7 +17,7 @@ nonempty : Type → Prop
 point : Type → Type → Type
 setoid : Type → Type
 subsingleton : Type → Prop
-well_founded : Π {A : Type}, (A → A → Prop) → Prop
+well_founded : Π {A}, (A → A → Prop) → Prop
 decidable : Prop → Type₁
 has_add : Type → Type
 has_div : Type → Type
@@ -37,4 +37,4 @@ nonempty : Type → Prop
 point : Type → Type → Type
 setoid : Type → Type
 subsingleton : Type → Prop
-well_founded : Π {A : Type}, (A → A → Prop) → Prop
+well_founded : Π {A}, (A → A → Prop) → Prop
diff --git a/tests/lean/subpp.lean.expected.out b/tests/lean/subpp.lean.expected.out
index e717499e7..00a7d56e9 100644
--- a/tests/lean/subpp.lean.expected.out
+++ b/tests/lean/subpp.lean.expected.out
@@ -1 +1 @@
-{x : ℕ | x > 0} : Type₁
+{x | x > 0} : Type₁
diff --git a/tests/lean/t11.lean.expected.out b/tests/lean/t11.lean.expected.out
index 43663bc41..f121ff9fd 100644
--- a/tests/lean/t11.lean.expected.out
+++ b/tests/lean/t11.lean.expected.out
@@ -1,3 +1,3 @@
-∃ (x : A), p x : bool
-∃ (x y : A), q x y : bool
-λ (x : A), x : A → A
+∃ x, p x : bool
+∃ x y, q x y : bool
+λ x, x : A → A
diff --git a/tests/lean/t12.lean.expected.out b/tests/lean/t12.lean.expected.out
index 0d908e700..382061120 100644
--- a/tests/lean/t12.lean.expected.out
+++ b/tests/lean/t12.lean.expected.out
@@ -1,2 +1,2 @@
-λ (f g : N → N → N) (x y : N), f x (g x y) : (N → N → N) → (N → N → N) → N → N → N
+λ f g x y, f x (g x y) : (N → N → N) → (N → N → N) → N → N → N
 t12.lean:7:7: error: invalid expression
diff --git a/tests/lean/t13.lean.expected.out b/tests/lean/t13.lean.expected.out
index e49c755af..d05d5480a 100644
--- a/tests/lean/t13.lean.expected.out
+++ b/tests/lean/t13.lean.expected.out
@@ -1,2 +1,2 @@
 [choice (g a b) (f a b)]
-λ (h : A → A → A), h a b : (A → A → A) → A
+λ h, h a b : (A → A → A) → A
diff --git a/tests/lean/unfold_rec.lean.expected.out b/tests/lean/unfold_rec.lean.expected.out
index b7a993e92..d4e87bf25 100644
--- a/tests/lean/unfold_rec.lean.expected.out
+++ b/tests/lean/unfold_rec.lean.expected.out
@@ -5,13 +5,13 @@ unfold_rec.lean:23:2: proof state
 n m : ℕ
 ⊢ succ (n + succ m) = succ (succ (n + m))
 unfold_rec.lean:38:2: proof state
-fibgt0 : ∀ (b n c : ℕ), fib ℕ b n c > 0,
+fibgt0 : ∀ b n c, fib ℕ b n c > 0,
 b m c : ℕ
 ⊢ fib ℕ b m c + fib ℕ b (succ m) c > 0
 unfold_rec.lean:47:2: proof state
 A : Type,
 B : Type,
-unzip_zip : ∀ {n : ℕ} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂),
+unzip_zip : ∀ {n} v₁ v₂, unzip (zip v₁ v₂) = (v₁, v₂),
 m : ℕ,
 a : A,
 va : vector A m,
diff --git a/tests/lean/univ_vars.lean.expected.out b/tests/lean/univ_vars.lean.expected.out
index 9c12fc386..e1fb09b5c 100644
--- a/tests/lean/univ_vars.lean.expected.out
+++ b/tests/lean/univ_vars.lean.expected.out
@@ -1,5 +1,5 @@
-id1 : Π (A : Type.{u}), A → A
-id2.{l_2} : Π (B : Type.{l_2}), B → B
-id3.{l_2} : Π (C : Type.{l_2}), C → C
-foo.{l_2} : Π (A₁ A₂ : Type.{l_2}), A₁ → A₂ → Prop
+id1 : Π A, A → A
+id2.{l_2} : Π B, B → B
+id3.{l_2} : Π C, C → C
+foo.{l_2} : Π A₁ A₂, A₁ → A₂ → Prop
 Type.{m} : Type.{m+1}
diff --git a/tests/lean/unsolved_proof_qed.lean.expected.out b/tests/lean/unsolved_proof_qed.lean.expected.out
index 481cc36c8..46fc1aa12 100644
--- a/tests/lean/unsolved_proof_qed.lean.expected.out
+++ b/tests/lean/unsolved_proof_qed.lean.expected.out
@@ -37,5 +37,5 @@ H₂ : b = c
 ⊢ c = a
 unsolved_proof_qed.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b c : ℕ) (H₁ : …) (H₂ : …),
+  λ a b c H₁ H₂,
     … ?M_1
diff --git a/tests/lean/urec.lean.expected.out b/tests/lean/urec.lean.expected.out
index 58e83c33b..2e84dfbc7 100644
--- a/tests/lean/urec.lean.expected.out
+++ b/tests/lean/urec.lean.expected.out
@@ -1,9 +1,7 @@
 urec.lean:3:0: error: invalid user defined recursor, result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables
 urec.lean:5:0: error: invalid user defined recursor, 'nat.rec' is a builtin recursor
 urec.lean:19:0: error: invalid user defined recursor, type of the major premise 'a' must be for the form (I ...), where I is a constant
-myrec.{l_1 l_2} :
-  Π (A : Type.{l_1}) (M : list.{l_1} A → Type.{l_2}) (l : list.{l_1} A),
-    M (@nil.{l_1} A) → (Π (a : A), M [a]) → (Π (a₁ a₂ : A), M [a₁, a₂]) → M l
+myrec.{l_1 l_2} : Π A M l, M (@nil.{l_1} A) → (Π a, M [a]) → (Π a₁ a₂, M [a₁, a₂]) → M l
 recursor information
   num. parameters:          1
   num. indices:             0
@@ -24,10 +22,8 @@ recursor information
   major premise pos.:       2
   dep. elimination:         1
 vector.induction_on.{l_1} :
-  ∀ {A : Type.{l_1}} {C : Π (a : ℕ), vector.{l_1} A a → Prop} {a : ℕ} (n : vector.{l_1} A a),
-    C 0 (@vector.nil.{l_1} A) →
-    (∀ {n : ℕ} (a : A) (a_1 : vector.{l_1} A n), C n a_1 → C (nat.succ n) (@vector.cons.{l_1} A n a a_1)) →
-    C a n
+  ∀ {A} {C} {a} n,
+    C 0 (@vector.nil.{l_1} A) → (∀ {n} a a_1, C n a_1 → C (nat.succ n) (@vector.cons.{l_1} A n a a_1)) → C a n
 recursor information
   num. parameters:          1
   num. indices:             1
@@ -39,9 +35,7 @@ recursor information
   dep. elimination:         1
   parameters pos. at major: 1
   indices pos. at major:    2
-Exists.rec.{l_1} :
-  ∀ {A : Type.{l_1}} {P : A → Prop} {C : Prop},
-    (∀ (a : A), P a → C) → @Exists.{l_1} A P → C
+Exists.rec.{l_1} : ∀ {A} {P} {C}, (∀ a, P a → C) → @Exists.{l_1} A P → C
 recursor information
   num. parameters:          2
   num. indices:             0
diff --git a/tests/lean/var2.lean.expected.out b/tests/lean/var2.lean.expected.out
index 743a819dc..ac563cf30 100644
--- a/tests/lean/var2.lean.expected.out
+++ b/tests/lean/var2.lean.expected.out
@@ -1 +1 @@
-foo : Π (B : Type), B → (Π (A : Type), A → A = B → Prop)
+foo : Π B, B → (Π A, A → A = B → Prop)
diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out
index 0c52b8723..4ee59deca 100644
--- a/tests/lean/whnf.lean.expected.out
+++ b/tests/lean/whnf.lean.expected.out
@@ -1,4 +1,4 @@
-succ (nat.rec 2 (λ (b₁ : ℕ), succ) 0)
+succ (nat.rec 2 (λ b₁, succ) 0)
 3
-succ (nat.rec a (λ (b₁ : ℕ), succ) 0)
+succ (nat.rec a (λ b₁, succ) 0)
 succ a