diff --git a/tests/lean/ex2.lean b/tests/lean/ex2.lean
index 219e901ba..15a869c74 100644
--- a/tests/lean/ex2.lean
+++ b/tests/lean/ex2.lean
@@ -1,5 +1,6 @@
 (* comment *)
 (* (* nested comment *) *)
+Set pp::colors false
 Show true
 Set lean::pp::notation false
 Show true && false
diff --git a/tests/lean/ex2.lean.expected.out b/tests/lean/ex2.lean.expected.out
index 1036e9302..5596fbefd 100644
--- a/tests/lean/ex2.lean.expected.out
+++ b/tests/lean/ex2.lean.expected.out
@@ -1,20 +1,21 @@
+  Set option: pp::colors
 ⊤
   Set option: lean::pp::notation
 and true false
   Assumed: a
-Error (line: 7, pos: 0) invalid object declaration, environment already has an object named 'a'
+Error (line: 8, pos: 0) invalid object declaration, environment already has an object named 'a'
   Assumed: b
 and a b
   Assumed: A
-Error (line: 11, pos: 11) type mismatch at application argument 2 of
+Error (line: 12, pos: 11) type mismatch at application argument 2 of
     and a A
 expected type
     Bool
 given type
-    Type
-Variable A : Type
-⟨lean::pp::notation ↦ false⟩
-Error (line: 14, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
-Error (line: 15, pos: 23) invalid option value, given option is not an integer
+    Type
+Variable A : Type
+⟨lean::pp::notation ↦ false, pp::colors ↦ false⟩
+Error (line: 15, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
+Error (line: 16, pos: 23) invalid option value, given option is not an integer
   Set option: lean::pp::notation
 a ∧ b
diff --git a/tests/lean/tst1.lean b/tests/lean/tst1.lean
index 28a8455e5..4e8ed0173 100644
--- a/tests/lean/tst1.lean
+++ b/tests/lean/tst1.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 (* Define a "fake" type to simulate the natural numbers. This is just a test. *)
 Variable N : Type
 Variable lt : N -> N -> Bool
diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out
index 0723a3783..08ffcc494 100644
--- a/tests/lean/tst1.lean.expected.out
+++ b/tests/lean/tst1.lean.expected.out
@@ -1,3 +1,4 @@
+  Set option: pp::colors
   Assumed: N
   Assumed: lt
   Assumed: zero
@@ -10,38 +11,38 @@
   Defined: update
   Defined: select
   Defined: map
-Axiom two_lt_three : two < three
-Definition vector (A : Type) (n : N) : Type := Π (i : N) (H : i < n), A
-Definition const {A : Type} (n : N) (d : A) : vector A n := λ (i : N) (H : i < n), d
-Definition const::explicit (A : Type) (n : N) (d : A) : vector A n := const n d
-Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n :=
-    λ (j : N) (H : j < n), if A (j = i) d (v j H)
-Definition update::explicit (A : Type) (n : N) (v : vector A n) (i : N) (d : A) : vector A n := update v i d
-Definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H
-Definition select::explicit (A : Type) (n : N) (v : vector A n) (i : N) (H : i < n) : A := select v i H
-Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
-    λ (i : N) (H : i < n), f (v1 i H) (v2 i H)
-Definition map::explicit (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
+Axiom two_lt_three : two < three
+Definition vector (A : Type) (n : N) : Type := Π (i : N) (H : i < n), A
+Definition const {A : Type} (n : N) (d : A) : vector A n := λ (i : N) (H : i < n), d
+Definition const::explicit (A : Type) (n : N) (d : A) : vector A n := const n d
+Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n :=
+    λ (j : N) (H : j < n), if A (j = i) d (v j H)
+Definition update::explicit (A : Type) (n : N) (v : vector A n) (i : N) (d : A) : vector A n := update v i d
+Definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H
+Definition select::explicit (A : Type) (n : N) (v : vector A n) (i : N) (H : i < n) : A := select v i H
+Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
+    λ (i : N) (H : i < n), f (v1 i H) (v2 i H)
+Definition map::explicit (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
     map f v1 v2
 Bool
 ⊤
 vector Bool three
 
 --------
-Π (A : Type) (n : N) (v : vector A n) (i : N) (H : i < n), A
+Π (A : Type) (n : N) (v : vector A n) (i : N) (H : i < n), A
 
 map type ---> 
-Π (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n), vector C n
+Π (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n), vector C n
 
 map normal form --> 
-λ (A B C : Type)
+λ (A B C : Type)
   (n : N)
-  (f : A → B → C)
-  (v1 : Π (i : N) (H : i < n), A)
-  (v2 : Π (i : N) (H : i < n), B)
+  (f : A → B → C)
+  (v1 : Π (i : N) (H : i < n), A)
+  (v2 : Π (i : N) (H : i < n), B)
   (i : N)
   (H : i < n),
   f (v1 i H) (v2 i H)
 
 update normal form --> 
-λ (A : Type) (n : N) (v : Π (i : N) (H : i < n), A) (i : N) (d : A) (j : N) (H : j < n), ite A (j = i) d (v j H)
+λ (A : Type) (n : N) (v : Π (i : N) (H : i < n), A) (i : N) (d : A) (j : N) (H : j < n), ite A (j = i) d (v j H)
diff --git a/tests/lean/tst10.lean b/tests/lean/tst10.lean
index d3413e0fb..a1454951a 100644
--- a/tests/lean/tst10.lean
+++ b/tests/lean/tst10.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Variable a : Bool
 Variable b : Bool
 (* Conjunctions *)
diff --git a/tests/lean/tst10.lean.expected.out b/tests/lean/tst10.lean.expected.out
index e985776c6..ef7040270 100644
--- a/tests/lean/tst10.lean.expected.out
+++ b/tests/lean/tst10.lean.expected.out
@@ -1,3 +1,4 @@
+  Set option: pp::colors
   Assumed: a
   Assumed: b
 a ∧ b
@@ -17,6 +18,6 @@ ite Bool a a ⊤
 a
   Assumed: H1
   Assumed: H2
-Π (a b : Bool) (H1 : a ⇒ b) (H2 : a), b
+Π (a b : Bool) (H1 : a ⇒ b) (H2 : a), b
 MP H2 H1
 b
diff --git a/tests/lean/tst11.lean b/tests/lean/tst11.lean
index a34f54bd3..9a4c99a32 100644
--- a/tests/lean/tst11.lean
+++ b/tests/lean/tst11.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Definition xor (x y : Bool) : Bool := (not x) = y
 Infixr 50 ⊕ : xor
 Show xor true false
diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out
index 264631a6d..74b68aad2 100644
--- a/tests/lean/tst11.lean.expected.out
+++ b/tests/lean/tst11.lean.expected.out
@@ -1,10 +1,11 @@
+  Set option: pp::colors
   Defined: xor
 ⊤ ⊕ ⊥
 ⊥
 ⊤
   Assumed: a
 a ⊕ a ⊕ a
-Π (A : Type u) (a b : A) (P : A → Bool) (H1 : P a) (H2 : a = b), P b
+Π (A : Type u) (a b : A) (P : A → Bool) (H1 : P a) (H2 : a = b), P b
   Proved: EM2
-Π a : Bool, a ∨ ¬ a
+Π a : Bool, a ∨ ¬ a
 a ∨ ¬ a
diff --git a/tests/lean/tst12.lean b/tests/lean/tst12.lean
index 74ff3a4b9..a163972c2 100644
--- a/tests/lean/tst12.lean
+++ b/tests/lean/tst12.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Show (fun x : Bool, (fun y : Bool, x /\ y))
 Show let x := true,
          y := true
diff --git a/tests/lean/tst12.lean.expected.out b/tests/lean/tst12.lean.expected.out
index 5f45439b1..bf208ff36 100644
--- a/tests/lean/tst12.lean.expected.out
+++ b/tests/lean/tst12.lean.expected.out
@@ -1,7 +1,8 @@
-λ x y : Bool, x ∧ y
-let x := ⊤,
-    y := ⊤,
-    z := x ∧ y,
-    f := λ arg1 arg2 : Bool, arg1 ∧ arg2 ⇔ arg2 ∧ arg1 ⇔ arg1 ∨ arg2 ∨ arg2
-in (f x y) ∨ z
+  Set option: pp::colors
+λ x y : Bool, x ∧ y
+let x := ⊤,
+    y := ⊤,
+    z := x ∧ y,
+    f := λ arg1 arg2 : Bool, arg1 ∧ arg2 ⇔ arg2 ∧ arg1 ⇔ arg1 ∨ arg2 ∨ arg2
+in (f x y) ∨ z
 ⊤
diff --git a/tests/lean/tst13.lean b/tests/lean/tst13.lean
index 6841ab845..0536677cf 100644
--- a/tests/lean/tst13.lean
+++ b/tests/lean/tst13.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Show fun x : Bool, (fun x : Bool, x).
 Show let x := true,
          y := true
diff --git a/tests/lean/tst13.lean.expected.out b/tests/lean/tst13.lean.expected.out
index a879ffc90..4658987a1 100644
--- a/tests/lean/tst13.lean.expected.out
+++ b/tests/lean/tst13.lean.expected.out
@@ -1,2 +1,3 @@
-λ x x : Bool, x
-let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in (f x y) ∨ z
+  Set option: pp::colors
+λ x x : Bool, x
+let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in (f x y) ∨ z
diff --git a/tests/lean/tst14.lean b/tests/lean/tst14.lean
index bc5ab03e2..262e5f5e9 100644
--- a/tests/lean/tst14.lean
+++ b/tests/lean/tst14.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Show Int -> Int -> Int
 Variable f : Int -> Int -> Int
 Eval f 0
diff --git a/tests/lean/tst14.lean.expected.out b/tests/lean/tst14.lean.expected.out
index ae8fd1a7a..e7a0ee738 100644
--- a/tests/lean/tst14.lean.expected.out
+++ b/tests/lean/tst14.lean.expected.out
@@ -1,5 +1,6 @@
-Int → Int → Int
+  Set option: pp::colors
+Int → Int → Int
   Assumed: f
 f 0
-Int → Int
+Int → Int
 Int
diff --git a/tests/lean/tst15.lean b/tests/lean/tst15.lean
index a6b54ddcd..2c8eb7ba2 100644
--- a/tests/lean/tst15.lean
+++ b/tests/lean/tst15.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Variable x : Type max u+1+2 m+1 m+2 3
 Check x
 Variable f : Type u+10 -> Type
diff --git a/tests/lean/tst15.lean.expected.out b/tests/lean/tst15.lean.expected.out
index d20403132..4fe2e8eaf 100644
--- a/tests/lean/tst15.lean.expected.out
+++ b/tests/lean/tst15.lean.expected.out
@@ -1,20 +1,21 @@
+  Set option: pp::colors
   Assumed: x
-Type u+3 ⊔ m+2 ⊔ 3
+Type u+3 ⊔ m+2 ⊔ 3
   Assumed: f
-Type u+10 → Type
-Type
-Type 5
-Type u+3 ⊔ m+2 ⊔ 3
-Type u+1 ⊔ m+1
-Type u+3
-Type u+4
-Type u+1 ⊔ m+1
-Type u+1 ⊔ m+1 ⊔ 4
-Type u+1 ⊔ m ⊔ 3
-Type u+2 ⊔ m+1 ⊔ 4
-Type u → Type 5
-Type u+1 ⊔ 6
-Type m+1 ⊔ 4 ⊔ u+6
-Type m ⊔ 3 → Type u → Type 5
-Type m+1 ⊔ 6 ⊔ u+1
-Type u
+Type u+10 → Type
+Type
+Type 5
+Type u+3 ⊔ m+2 ⊔ 3
+Type u+1 ⊔ m+1
+Type u+3
+Type u+4
+Type u+1 ⊔ m+1
+Type u+1 ⊔ m+1 ⊔ 4
+Type u+1 ⊔ m ⊔ 3
+Type u+2 ⊔ m+1 ⊔ 4
+Type u → Type 5
+Type u+1 ⊔ 6
+Type m+1 ⊔ 4 ⊔ u+6
+Type m ⊔ 3 → Type u → Type 5
+Type m+1 ⊔ 6 ⊔ u+1
+Type u
diff --git a/tests/lean/tst16.lean b/tests/lean/tst16.lean
index ce0732e90..90768808f 100644
--- a/tests/lean/tst16.lean
+++ b/tests/lean/tst16.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Variable f : Type -> Bool
 Show forall a b : Type, (f a) = (f b)
 Variable g : Bool -> Bool -> Bool
diff --git a/tests/lean/tst16.lean.expected.out b/tests/lean/tst16.lean.expected.out
index e2062caa3..f9978a85e 100644
--- a/tests/lean/tst16.lean.expected.out
+++ b/tests/lean/tst16.lean.expected.out
@@ -1,14 +1,15 @@
+  Set option: pp::colors
   Assumed: f
-∀ a b : Type, (f a) = (f b)
+∀ a b : Type, (f a) = (f b)
   Assumed: g
-∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
-∃ (a b : Type) (c : Bool), g c ((f a) = (f b))
-∀ (a b : Type) (c : Bool), (g c (f a)) = (f b) ⇒ (f a)
+∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
+∃ (a b : Type) (c : Bool), g c ((f a) = (f b))
+∀ (a b : Type) (c : Bool), (g c (f a)) = (f b) ⇒ (f a)
 Bool
-∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
-∀ a b : Type, (f a) = (f b)
-∃ a b : Type, (f a) = (f b) ∧ (f a)
-∃ a b : Type, (f a) = (f b) ∨ (f b)
+∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
+∀ a b : Type, (f a) = (f b)
+∃ a b : Type, (f a) = (f b) ∧ (f a)
+∃ a b : Type, (f a) = (f b) ∨ (f b)
   Assumed: a
 (f a) ∨ (f a)
 (f a) = a ∨ (f a)
diff --git a/tests/lean/tst17.lean b/tests/lean/tst17.lean
index c335b8f2e..95083cfab 100644
--- a/tests/lean/tst17.lean
+++ b/tests/lean/tst17.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Variable f : Type -> Bool
 Variable g : Type -> Type -> Bool
 Show forall (a b : Type), exists (c : Type), (g a b) = (f c)
diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out
index 411fc2eea..cf3289bc4 100644
--- a/tests/lean/tst17.lean.expected.out
+++ b/tests/lean/tst17.lean.expected.out
@@ -1,8 +1,9 @@
+  Set option: pp::colors
   Assumed: f
   Assumed: g
-∀ a b : Type, ∃ c : Type, (g a b) = (f c)
+∀ a b : Type, ∃ c : Type, (g a b) = (f c)
 Bool
-(λ a : Type,
-   (λ b : Type, ite Bool ((λ x : Type, ite Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) =
-   (λ x : Type, ⊤)) =
-(λ x : Type, ⊤)
+(λ a : Type,
+   (λ b : Type, ite Bool ((λ x : Type, ite Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) =
+   (λ x : Type, ⊤)) =
+(λ x : Type, ⊤)
diff --git a/tests/lean/tst3.lean b/tests/lean/tst3.lean
index a7f68b0cd..ccf5d81a0 100644
--- a/tests/lean/tst3.lean
+++ b/tests/lean/tst3.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Set lean::parser::verbose false.
 Notation 10 if _ then _ : implies.
 Show Environment 1.
diff --git a/tests/lean/tst3.lean.expected.out b/tests/lean/tst3.lean.expected.out
index bbc747917..36b17a092 100644
--- a/tests/lean/tst3.lean.expected.out
+++ b/tests/lean/tst3.lean.expected.out
@@ -1,8 +1,9 @@
-Notation 10 if _ then _ : implies
+  Set option: pp::colors
+Notation 10 if _ then _ : implies
 if ⊤ then ⊥
 if ⊤ then (if a then ⊥)
 implies true (implies a false)
-Notation 100 _ |- _ ; _ : f
+Notation 100 _ |- _ ; _ : f
 f c d e
 c |- d ; e
 (a !) !
@@ -10,7 +11,7 @@ fact (fact a)
 [ c ; d ]
 [ c ; ([ d ; e ]) ]
 g c (g d e)
-Notation 40 _ << _ end : h
+Notation 40 _ << _ end : h
 d << e end
 [ c ; d << e end ]
 g c (h d e)
diff --git a/tests/lean/tst4.lean b/tests/lean/tst4.lean
index aa5236d00..0bd1fc821 100644
--- a/tests/lean/tst4.lean
+++ b/tests/lean/tst4.lean
@@ -7,6 +7,7 @@ Show f n1 n2
 Show f (fun x : N -> N, x) (fun y : _, y)
 Variable EqNice {A : Type} (lhs rhs : A) : Bool
 Infix 50 === : EqNice
+Set pp::colors false
 Show n1 === n2
 Check f n1 n2
 Check Congr::explicit
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index 494c83863..f6f3e57eb 100644
--- a/tests/lean/tst4.lean.expected.out
+++ b/tests/lean/tst4.lean.expected.out
@@ -6,9 +6,10 @@
 f::explicit N n1 n2
 f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
   Assumed: EqNice
+  Set option: pp::colors
 EqNice::explicit N n1 n2
 N
-Π (A : Type u) (B : A → Type u) (f g : Π x : A, B x) (a b : A) (H1 : f = g) (H2 : a = b), (f a) = (g b)
+Π (A : Type u) (B : A → Type u) (f g : Π x : A, B x) (a b : A) (H1 : f = g) (H2 : a = b), (f a) = (g b)
 f::explicit N n1 n2
   Assumed: a
   Assumed: b
@@ -16,13 +17,13 @@ f::explicit N n1 n2
   Assumed: g
   Assumed: H1
   Proved: Pr
-Axiom H1 : a = b ∧ b = c
-Theorem Pr : (g a) = (g c) :=
-    let κ::1 := Trans::explicit
+Axiom H1 : a = b ∧ b = c
+Theorem Pr : (g a) = (g c) :=
+    let κ::1 := Trans::explicit
                      N
                      a
                      b
                      c
                      (Conjunct1::explicit (a = b) (b = c) H1)
                      (Conjunct2::explicit (a = b) (b = c) H1)
-    in Congr::explicit N (λ x : N, N) g g a c (Refl::explicit (N → N) g) κ::1
+    in Congr::explicit N (λ x : N, N) g g a c (Refl::explicit (N → N) g) κ::1
diff --git a/tests/lean/tst5.lean b/tests/lean/tst5.lean
index 11444d46c..1f0297d6a 100644
--- a/tests/lean/tst5.lean
+++ b/tests/lean/tst5.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Variable N : Type
 Variable a : N
 Variable b : N
diff --git a/tests/lean/tst5.lean.expected.out b/tests/lean/tst5.lean.expected.out
index 26e2ec5f0..481cff1a6 100644
--- a/tests/lean/tst5.lean.expected.out
+++ b/tests/lean/tst5.lean.expected.out
@@ -1,3 +1,4 @@
+  Set option: pp::colors
   Assumed: N
   Assumed: a
   Assumed: b
@@ -5,5 +6,5 @@ a ≃ b
 Bool
   Set option: 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 ⊤ ⊥
diff --git a/tests/lean/tst6.lean b/tests/lean/tst6.lean
index e13f1eab9..e63041696 100644
--- a/tests/lean/tst6.lean
+++ b/tests/lean/tst6.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Variable N : Type
 Variable h : N -> N -> N
 
diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out
index a04b66c42..782dd0250 100644
--- a/tests/lean/tst6.lean.expected.out
+++ b/tests/lean/tst6.lean.expected.out
@@ -1,31 +1,32 @@
+  Set option: pp::colors
   Assumed: N
   Assumed: h
   Proved: CongrH
   Set option: lean::pp::implicit
-Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
+Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
     Congr::explicit
         N
-        (λ x : N, N)
+        (λ x : N, N)
         (h a1)
         (h b1)
         a2
         b2
-        (Congr::explicit N (λ x : N, N → N) h h a1 b1 (Refl::explicit (N → N → N) h) H1)
+        (Congr::explicit N (λ x : N, N → N) h h a1 b1 (Refl::explicit (N → N → N) h) H1)
         H2
-Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
+Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
     CongrH::explicit a1 a2 b1 b2 H1 H2
   Set option: lean::pp::implicit
-Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Congr (Congr (Refl h) H1) H2
-Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
+Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Congr (Congr (Refl h) H1) H2
+Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
   Proved: Example1
   Set option: lean::pp::implicit
-Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
+Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
     DisjCases::explicit
         (a = b ∧ b = c)
         (a = d ∧ d = c)
         ((h a b) = (h c b))
         H
-        (λ H1 : a = b ∧ b = c,
+        (λ H1 : a = b ∧ b = c,
            CongrH::explicit
                a
                b
@@ -39,7 +40,7 @@
                     (Conjunct1::explicit (a = b) (b = c) H1)
                     (Conjunct2::explicit (a = b) (b = c) H1))
                (Refl::explicit N b))
-        (λ H1 : a = d ∧ d = c,
+        (λ H1 : a = d ∧ d = c,
            CongrH::explicit
                a
                b
@@ -55,13 +56,13 @@
                (Refl::explicit N b))
   Proved: Example2
   Set option: lean::pp::implicit
-Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
+Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
     DisjCases::explicit
         (a = b ∧ b = c)
         (a = d ∧ d = c)
         ((h a b) = (h c b))
         H
-        (λ H1 : a = b ∧ b = c,
+        (λ H1 : a = b ∧ b = c,
            CongrH::explicit
                a
                b
@@ -75,7 +76,7 @@
                     (Conjunct1::explicit (a = b) (b = c) H1)
                     (Conjunct2::explicit (a = b) (b = c) H1))
                (Refl::explicit N b))
-        (λ H1 : a = d ∧ d = c,
+        (λ H1 : a = d ∧ d = c,
            CongrH::explicit
                a
                b
@@ -91,16 +92,16 @@
                (Refl::explicit N b))
   Proved: Example3
   Set option: lean::pp::implicit
-Theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
+Theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
     DisjCases
         H
-        (λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b))
-        (λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
+        (λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b))
+        (λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
   Proved: Example4
   Set option: lean::pp::implicit
-Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
+Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
     DisjCases
         H
-        (λ H1 : a = b ∧ b = e ∧ b = c,
-           let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
-        (λ H1 : a = d ∧ d = c, let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))
+        (λ H1 : a = b ∧ b = e ∧ b = c,
+           let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
+        (λ H1 : a = d ∧ d = c, let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))
diff --git a/tests/lean/tst7.lean b/tests/lean/tst7.lean
index d896e8ab3..5292774c4 100644
--- a/tests/lean/tst7.lean
+++ b/tests/lean/tst7.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Variable f : Pi (A : Type), A -> Bool
 Show fun (A B : Type) (a : _), f B a
 (* The following one should produce an error *)
diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out
index 4e384d1e2..a6883ba26 100644
--- a/tests/lean/tst7.lean.expected.out
+++ b/tests/lean/tst7.lean.expected.out
@@ -1,14 +1,15 @@
+  Set option: pp::colors
   Assumed: f
-λ (A B : Type) (a : B), f B a
-Error (line: 4, pos: 40) application type mismatch during term elaboration at term
+λ (A B : Type) (a : B), f B a
+Error (line: 5, pos: 40) application type mismatch during term elaboration at term
     f B a
 Elaborator state
-    ?M0 := [unassigned]
-    ?M1 := [unassigned]
-    #0 ≈ lift:0:2 ?M0
+    ?M0 := [unassigned]
+    ?M1 := [unassigned]
+    #0 ≈ lift:0:2 ?M0
   Assumed: myeq
-myeq (Π (A : Type) (a : A), A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b)
+myeq (Π (A : Type) (a : A), A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b)
 Bool
   Assumed: R
   Assumed: h
-Bool → (Π (f1 g1 : Π A : Type, R A) (G : Π A : Type, myeq (R A) (f1 A) (g1 A)), Bool)
+Bool → (Π (f1 g1 : Π A : Type, R A) (G : Π A : Type, myeq (R A) (f1 A) (g1 A)), Bool)
diff --git a/tests/lean/tst8.lean b/tests/lean/tst8.lean
index 6aef8a164..c047e451a 100644
--- a/tests/lean/tst8.lean
+++ b/tests/lean/tst8.lean
@@ -1,3 +1,4 @@
+Set pp::colors false
 Check fun (A : Type) (a : A),
           let b := a
           in b
diff --git a/tests/lean/tst8.lean.expected.out b/tests/lean/tst8.lean.expected.out
index 9821726c6..694bdd014 100644
--- a/tests/lean/tst8.lean.expected.out
+++ b/tests/lean/tst8.lean.expected.out
@@ -1,3 +1,4 @@
-Π (A : Type) (a : A), A
+  Set option: pp::colors
+Π (A : Type) (a : A), A
   Assumed: g
   Defined: f