diff --git a/tests/lean/conv.lean.expected.out b/tests/lean/conv.lean.expected.out
index 5a971a7fd..0cbd5fad7 100644
--- a/tests/lean/conv.lean.expected.out
+++ b/tests/lean/conv.lean.expected.out
@@ -11,9 +11,9 @@ p f : Bool
 g a : Bool
   Defined: c2
   Assumed: b
-c2::explicit : Π (T : Type), Type 3 → T → Type 3
+c2::explicit : Π (T : Type), (Type 3) → T → (Type 3)
   Assumed: g2
-g2 : (c2 Type 2 b) → Bool
+g2 : (c2 (Type 2) b) → Bool
   Assumed: a2
 g2 a2 : Bool
-λ x : c2 Type 1 b, g2 x : (c2 Type 1 b) → Bool
+λ x : c2 (Type 1) b, g2 x : (c2 (Type 1) b) → Bool
diff --git a/tests/lean/tst15.lean.expected.out b/tests/lean/tst15.lean.expected.out
index e02734039..19d8e17de 100644
--- a/tests/lean/tst15.lean.expected.out
+++ b/tests/lean/tst15.lean.expected.out
@@ -3,7 +3,7 @@
   Assumed: x
 x : Type U+3 ⊔ M+2 ⊔ 3
   Assumed: f
-f : Type U+10 → Type
+f : (Type U+10) → Type
 f x : Type
 Type 4 : Type 5
 x : Type U+3 ⊔ M+2 ⊔ 3
@@ -14,9 +14,9 @@ Type U ⊔ M : Type U+1 ⊔ M+1
 Type U ⊔ M ⊔ 3 : Type U+1 ⊔ M+1 ⊔ 4
 Type U+1 ⊔ M ⊔ 3
 Type U+1 ⊔ M ⊔ 3 : Type U+2 ⊔ M+1 ⊔ 4
-Type U → Type 5
-Type U → Type 5 : Type U+1 ⊔ 6
-Type M ⊔ 3 → Type U+5 : Type M+1 ⊔ 4 ⊔ U+6
-Type M ⊔ 3 → Type U → Type 5
-Type M ⊔ 3 → Type U → Type 5 : Type M+1 ⊔ 6 ⊔ U+1
+(Type U) → (Type 5)
+(Type U) → (Type 5) : Type U+1 ⊔ 6
+(Type M ⊔ 3) → (Type U+5) : Type M+1 ⊔ 4 ⊔ U+6
+(Type M ⊔ 3) → (Type U) → (Type 5)
+(Type M ⊔ 3) → (Type U) → (Type 5) : Type M+1 ⊔ 6 ⊔ U+1
 Type U
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index ad0c6ba60..02f6ed932 100644
--- a/tests/lean/tst4.lean.expected.out
+++ b/tests/lean/tst4.lean.expected.out
@@ -11,7 +11,7 @@ f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
 EqNice::explicit N n1 n2
 f::explicit N n1 n2 : N
 Congr::explicit :
-    Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A), (f = g) → (a = b) → ((f a) = (g b))
+    Π (A : Type U) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), (f = g) → (a = b) → ((f a) = (g b))
 f::explicit N n1 n2
   Assumed: a
   Assumed: b
diff --git a/tests/lean/tst5.lean.expected.out b/tests/lean/tst5.lean.expected.out
index 9f878e181..859c33074 100644
--- a/tests/lean/tst5.lean.expected.out
+++ b/tests/lean/tst5.lean.expected.out
@@ -7,5 +7,5 @@ a ≃ b
 a ≃ b : Bool
   Set: lean::pp::implicit
 heq::explicit N a b
-heq::explicit Type 2 Type 1 Type 1
+heq::explicit (Type 2) (Type 1) (Type 1)
 heq::explicit Bool ⊤ ⊥