diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp
index 0b8fbb738..6dde7d299 100644
--- a/src/frontends/lean/notation.cpp
+++ b/src/frontends/lean/notation.cpp
@@ -15,10 +15,9 @@ namespace lean {
    \brief Initialize builtin notation.
 */
 void init_builtin_notation(frontend & f) {
+    f.add_infix("=",  50, mk_homo_eq_fn());
     f.mark_implicit_arguments(mk_homo_eq_fn(), {true, false, false});
     f.mark_implicit_arguments(mk_if_fn(), {true, false, false, false});
-    f.add_infix("==", 50, mk_homo_eq_fn());
-    f.add_infix("≃",  50, mk_homo_eq_fn());
 
     f.add_prefix("\u00ac", 40, mk_not_fn());     // "¬"
     f.add_infixr("&&", 35, mk_and_fn());         // "&&"
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index f6a7b0da1..4e4dea7d9 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -57,7 +57,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static format g_Type_fmt      = highlight_builtin(format("Type"));
-static format g_eq_fmt        = format("=");
+static format g_eq_fmt        = format("==");
 static format g_lambda_n_fmt  = highlight_keyword(format("\u03BB"));
 static format g_Pi_n_fmt      = highlight_keyword(format("\u03A0"));
 static format g_lambda_fmt    = highlight_keyword(format("fun"));
diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index a2665eace..e43959ab4 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -22,7 +22,7 @@ static name g_pi_name("Pi");
 static name g_let_name("let");
 static name g_in_name("in");
 static name g_arrow_name("->");
-static name g_eq_name("=");
+static name g_eq_name("==");
 static name g_forall_name("forall");
 static name g_forall_unicode("\u2200");
 static name g_exists_name("exists");
@@ -393,7 +393,7 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
     case scanner::token::NatVal:            out << "Nat"; break;
     case scanner::token::DecimalVal:        out << "Dec"; break;
     case scanner::token::StringVal:         out << "String"; break;
-    case scanner::token::Eq:                out << "="; break;
+    case scanner::token::Eq:                out << "=="; break;
     case scanner::token::Assign:            out << ":="; break;
     case scanner::token::Type:              out << "Type"; break;
     case scanner::token::Placeholder:       out << "_"; break;
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index e68c89153..1d01e6d05 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -155,7 +155,7 @@ MK_CONSTANT(or_fn,      name("or"));
 MK_CONSTANT(not_fn,     name("not"));
 MK_CONSTANT(forall_fn,  name("forall"));
 MK_CONSTANT(exists_fn,  name("exists"));
-MK_CONSTANT(homo_eq_fn, name("heq"));
+MK_CONSTANT(homo_eq_fn, name("eq"));
 
 // Axioms
 MK_CONSTANT(mp_fn,          name("MP"));
diff --git a/src/kernel/printer.cpp b/src/kernel/printer.cpp
index 528a5b219..e07f6c80f 100644
--- a/src/kernel/printer.cpp
+++ b/src/kernel/printer.cpp
@@ -56,7 +56,7 @@ struct print_expr_fn {
 
     void print_eq(expr const & a, context const & c) {
         print_child(eq_lhs(a), c);
-        out() << " = ";
+        out() << " == ";
         print_child(eq_rhs(a), c);
     }
 
diff --git a/src/tests/library/formatter.cpp b/src/tests/library/formatter.cpp
index 382ae7636..1f6b9a57a 100644
--- a/src/tests/library/formatter.cpp
+++ b/src/tests/library/formatter.cpp
@@ -16,7 +16,7 @@ static void check(format const & f, char const * expected) {
     std::ostringstream strm;
     strm << f;
     std::cout << strm.str() << "\n";
-    lean_assert(strm.str() == expected);
+    lean_assert_eq(strm.str(), expected);
 }
 
 static void tst1() {
@@ -30,15 +30,15 @@ static void tst1() {
     expr y  = Const("y");
     expr N  = Const("N");
     expr F  = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(Eq(x, f(y, a)))));
-    check(fmt(F), "fun x : (Pi x : N, (x -> x)), (let y := f a in (f (x = (f y a))))");
+    check(fmt(F), "fun x : (Pi x : N, (x -> x)), (let y := f a in (f (x == (f y a))))");
     check(fmt(env.get_object("N")), "Variable N : Type");
     context ctx;
     ctx = extend(ctx, "x", f(a));
     ctx = extend(ctx, "y", f(Var(0), N >> N));
     ctx = extend(ctx, "z", N, Eq(Var(0), Var(1)));
-    check(fmt(ctx), "[x : f a; y : f x (N -> N); z : N := y = x]");
+    check(fmt(ctx), "[x : f a; y : f x (N -> N); z : N := y == x]");
     check(fmt(ctx, f(Var(0), Var(2))), "f z x");
-    check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x (N -> N); z : N := y = x] |- f z x");
+    check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x (N -> N); z : N := y == x] |- f z x");
     fmt.set_interrupt(true);
     fmt.set_interrupt(false);
 }
diff --git a/tests/lean/arith6.lean.expected.out b/tests/lean/arith6.lean.expected.out
index 37825dc8a..ce817104b 100644
--- a/tests/lean/arith6.lean.expected.out
+++ b/tests/lean/arith6.lean.expected.out
@@ -7,8 +7,8 @@ false
 true
 true
   Assumed: x
-3 + -1 * (x * (3 div x)) = 0
-x + -1 * (3 * (x div 3)) = 0
+3 + -1 * (x * (3 div x)) == 0
+x + -1 * (3 * (x div 3)) == 0
 false
   Set: lean::pp::notation
 Int::divides 3 x
diff --git a/tests/lean/cast2.lean.expected.out b/tests/lean/cast2.lean.expected.out
index b737cb856..53d678f68 100644
--- a/tests/lean/cast2.lean.expected.out
+++ b/tests/lean/cast2.lean.expected.out
@@ -6,7 +6,7 @@
   Assumed: B'
   Assumed: H
   Assumed: a
-DomInj H : A = A'
+DomInj H : A == A'
   Proved: BeqB'
   Set: lean::pp::implicit
 DomInj::explicit A A' (λ x : A, B) (λ x : A', B') H
diff --git a/tests/lean/cast3.lean.expected.out b/tests/lean/cast3.lean.expected.out
index e8b99396e..c510b2029 100644
--- a/tests/lean/cast3.lean.expected.out
+++ b/tests/lean/cast3.lean.expected.out
@@ -6,7 +6,7 @@
   Assumed: B'
   Assumed: x
 x
-x = x
+x == x
   Assumed: b
   Defined: f
   Assumed: H
diff --git a/tests/lean/elab1.lean b/tests/lean/elab1.lean
index e66f34937..69952a74e 100644
--- a/tests/lean/elab1.lean
+++ b/tests/lean/elab1.lean
@@ -10,9 +10,9 @@ Variable h : Pi (A : Type), A -> A.
 
 Check fun x, fun A : Type, h A x
 
-Variable eq : Pi A : Type, A -> A -> Bool.
+Variable my_eq : Pi A : Type, A -> A -> Bool.
 
-Check fun (A B : Type) (a : _) (b : _) (C : Type), eq C a b.
+Check fun (A B : Type) (a : _) (b : _) (C : Type), my_eq C a b.
 
 Variable a : Bool
 Variable b : Bool
diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out
index 539db6df8..7fb9cea85 100644
--- a/tests/lean/elab1.lean.expected.out
+++ b/tests/lean/elab1.lean.expected.out
@@ -123,11 +123,11 @@ x : ?M3::0, A : Type ⊢ ?M3::0[lift:0:2] ≺ A
     with arguments:
         A
         x
-  Assumed: eq
+  Assumed: my_eq
 Failed to solve
 A : Type, B : Type, a : ?M3::0, b : ?M3::1, C : Type ⊢ ?M3::0[lift:0:3] ≺ C
     (line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of
-        eq
+        my_eq
     with arguments:
         C
         a
@@ -139,29 +139,29 @@ Error (line: 20, pos: 28) unexpected metavariable occurrence
 Failed to solve
  ⊢ b ≈ a
     Substitution
-     ⊢ b ≈ ?M3::2
+     ⊢ b ≈ ?M3::3
         Destruct/Decompose
-         ⊢ b = b ≺ ?M3::2 = ?M3::3
+         ⊢ b == b ≺ ?M3::3 == ?M3::4
             (line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of
                 Trans::explicit
             with arguments:
-                ?M3::0
                 ?M3::1
                 ?M3::2
                 ?M3::3
+                ?M3::4
                 Refl a
                 Refl b
         Assignment
-         ⊢ a ≈ ?M3::2
+         ⊢ a ≈ ?M3::3
             Destruct/Decompose
-             ⊢ a = a ≺ ?M3::1 = ?M3::2
+             ⊢ a == a ≺ ?M3::2 == ?M3::3
                 (line: 22: pos: 22) Type of argument 5 must be convertible to the expected type in the application of
                     Trans::explicit
                 with arguments:
-                    ?M3::0
                     ?M3::1
                     ?M3::2
                     ?M3::3
+                    ?M3::4
                     Refl a
                     Refl b
 Failed to solve
diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out
index 30a839e56..4006b0d93 100644
--- a/tests/lean/elab4.lean.expected.out
+++ b/tests/lean/elab4.lean.expected.out
@@ -5,19 +5,24 @@
   Assumed: R
   Proved: R2
   Set: lean::pp::implicit
-Variable C {A B : Type} (H : A = B) (a : A) : B
+Variable C {A B : Type} (H : eq::explicit Type A B) (a : A) : B
 Definition C::explicit (A B : Type) (H : A = B) (a : A) : B := C H a
-Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) : A = A'
+Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) :
+    eq::explicit Type A A'
 Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (Π x : A, B x) = (Π x : A', B' x)) : A =
     A' :=
     D H
-Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) (a : A) :
-    (B a) = (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
+Variable R {A A' : Type}
+    {B : A → Type}
+    {B' : A' → Type}
+    (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x))
+    (a : A) :
+    eq::explicit Type (B a) (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
 Definition R::explicit (A A' : Type)
     (B : A → Type)
     (B' : A' → Type)
     (H : (Π x : A, B x) = (Π x : A', B' x))
     (a : A) : (B a) = (B' (C (D H) a)) :=
     R H a
-Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
+Theorem R2 (A1 A2 B1 B2 : Type) (H : eq::explicit Type (A1 → B1) (A2 → B2)) (a : A1) : eq::explicit Type B1 B2 :=
     R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a
diff --git a/tests/lean/elab5.lean.expected.out b/tests/lean/elab5.lean.expected.out
index 30a839e56..4006b0d93 100644
--- a/tests/lean/elab5.lean.expected.out
+++ b/tests/lean/elab5.lean.expected.out
@@ -5,19 +5,24 @@
   Assumed: R
   Proved: R2
   Set: lean::pp::implicit
-Variable C {A B : Type} (H : A = B) (a : A) : B
+Variable C {A B : Type} (H : eq::explicit Type A B) (a : A) : B
 Definition C::explicit (A B : Type) (H : A = B) (a : A) : B := C H a
-Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) : A = A'
+Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) :
+    eq::explicit Type A A'
 Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (Π x : A, B x) = (Π x : A', B' x)) : A =
     A' :=
     D H
-Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) (a : A) :
-    (B a) = (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
+Variable R {A A' : Type}
+    {B : A → Type}
+    {B' : A' → Type}
+    (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x))
+    (a : A) :
+    eq::explicit Type (B a) (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
 Definition R::explicit (A A' : Type)
     (B : A → Type)
     (B' : A' → Type)
     (H : (Π x : A, B x) = (Π x : A', B' x))
     (a : A) : (B a) = (B' (C (D H) a)) :=
     R H a
-Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
+Theorem R2 (A1 A2 B1 B2 : Type) (H : eq::explicit Type (A1 → B1) (A2 → B2)) (a : A1) : eq::explicit Type B1 B2 :=
     R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a
diff --git a/tests/lean/eq1.lean b/tests/lean/eq1.lean
new file mode 100644
index 000000000..8af2b670b
--- /dev/null
+++ b/tests/lean/eq1.lean
@@ -0,0 +1,5 @@
+
+Variable i : Int
+Check i = 0
+Set pp::coercion true
+Check i = 0
diff --git a/tests/lean/eq1.lean.expected.out b/tests/lean/eq1.lean.expected.out
new file mode 100644
index 000000000..aa59ac42e
--- /dev/null
+++ b/tests/lean/eq1.lean.expected.out
@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: i
+i = 0 : Bool
+  Set: lean::pp::coercion
+i = (nat_to_int 0) : Bool
diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out
index ff9a7e0a6..89f98d1fa 100644
--- a/tests/lean/tst1.lean.expected.out
+++ b/tests/lean/tst1.lean.expected.out
@@ -26,7 +26,7 @@ Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2
 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
 select (update (const three ⊥) two ⊤) two two_lt_three : Bool
-if (two = two) ⊤ ⊥
+if (two == two) ⊤ ⊥
 update (const three ⊥) two ⊤ : vector Bool three
 
 --------
@@ -46,4 +46,4 @@ map normal form -->
   f (v1 i H) (v2 i H)
 
 update normal form --> 
-λ (A : Type) (n : N) (v : Π (i : N), (i < n) → A) (i : N) (d : A) (j : N) (H : j < n), if (j = i) d (v j H)
+λ (A : Type) (n : N) (v : Π (i : N), (i < n) → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) d (v j H)
diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out
index 3901abab3..be6893f83 100644
--- a/tests/lean/tst11.lean.expected.out
+++ b/tests/lean/tst11.lean.expected.out
@@ -6,7 +6,7 @@
 ⊤
   Assumed: a
 a ⊕ a ⊕ a
-Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → (a = b) → (P b)
+Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → (a == b) → (P b)
   Proved: EM2
 EM2 : Π a : Bool, a ∨ ¬ a
 EM2 a : a ∨ ¬ a
diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out
index 8238bde24..01155a2e8 100644
--- a/tests/lean/tst17.lean.expected.out
+++ b/tests/lean/tst17.lean.expected.out
@@ -5,5 +5,6 @@
 ∀ 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, if ((λ x : Type, if ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) = (λ x : Type, ⊤)) =
+   (λ b : Type, if ((λ x : Type, if ((g a b) == (f x)) ⊥ ⊤) == (λ x : Type, ⊤)) ⊥ ⊤) ==
+   (λ x : Type, ⊤)) ==
 (λ x : Type, ⊤)
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index 02f6ed932..2603e134e 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
@@ -19,8 +19,8 @@ f::explicit N n1 n2
   Assumed: g
   Assumed: H1
   Proved: Pr
-Axiom H1 : a = b ∧ b = c
-Theorem Pr : (g a) = (g c) :=
+Axiom H1 : eq::explicit N a b ∧ eq::explicit N b c
+Theorem Pr : eq::explicit N (g a) (g c) :=
     Congr::explicit
         N
         (λ x : N, N)
@@ -29,4 +29,10 @@ Theorem Pr : (g a) = (g c) :=
         a
         c
         (Refl::explicit (N → N) g)
-        (Trans::explicit N a b c (Conjunct1::explicit (a = b) (b = c) H1) (Conjunct2::explicit (a = b) (b = c) H1))
+        (Trans::explicit
+             N
+             a
+             b
+             c
+             (Conjunct1::explicit (eq::explicit N a b) (eq::explicit N b c) H1)
+             (Conjunct2::explicit (eq::explicit N a b) (eq::explicit N b c) H1))
diff --git a/tests/lean/tst5.lean b/tests/lean/tst5.lean
index 11444d46c..bc57f3169 100644
--- a/tests/lean/tst5.lean
+++ b/tests/lean/tst5.lean
@@ -1,9 +1,9 @@
 Variable N : Type
 Variable a : N
 Variable b : N
-Show a ≃ b
-Check a ≃ b
+Show a = b
+Check a = b
 Set lean::pp::implicit true
-Show a ≃ b
-Show (Type 1) ≃ (Type 1)
-Show true ≃ false
+Show a = b
+Show (Type 1) = (Type 1)
+Show true = false
diff --git a/tests/lean/tst5.lean.expected.out b/tests/lean/tst5.lean.expected.out
index 859c33074..64220b01e 100644
--- a/tests/lean/tst5.lean.expected.out
+++ b/tests/lean/tst5.lean.expected.out
@@ -3,9 +3,9 @@
   Assumed: N
   Assumed: a
   Assumed: b
-a ≃ b
-a ≃ b : Bool
+a = b
+a = b : Bool
   Set: lean::pp::implicit
-heq::explicit N a b
-heq::explicit (Type 2) (Type 1) (Type 1)
-heq::explicit Bool ⊤ ⊥
+eq::explicit N a b
+eq::explicit (Type 2) (Type 1) (Type 1)
+eq::explicit Bool ⊤ ⊥
diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out
index e63242bbd..2356f95d5 100644
--- a/tests/lean/tst6.lean.expected.out
+++ b/tests/lean/tst6.lean.expected.out
@@ -4,7 +4,10 @@
   Assumed: h
   Proved: CongrH
   Set: 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 : eq::explicit N a1 b1) (H2 : eq::explicit N a2 b2) : eq::explicit
+        N
+        (h a1 a2)
+        (h b1 b2) :=
     Congr::explicit
         N
         (λ x : N, N)
@@ -20,13 +23,17 @@ Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h
 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: 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 : eq::explicit N a b ∧ eq::explicit N b c ∨ eq::explicit N a d ∧ eq::explicit N d c) : eq::explicit
+        N
+        (h a b)
+        (h c b) :=
     DisjCases::explicit
-        (a = b ∧ b = c)
-        (a = d ∧ d = c)
-        ((h a b) = (h c b))
+        (eq::explicit N a b ∧ eq::explicit N b c)
+        (eq::explicit N a d ∧ eq::explicit N d c)
+        ((h a b) == (h c b))
         H
-        (λ H1 : a = b ∧ b = c,
+        (λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
            CongrH::explicit
                a
                b
@@ -37,10 +44,10 @@ Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
                     a
                     b
                     c
-                    (Conjunct1::explicit (a = b) (b = c) H1)
-                    (Conjunct2::explicit (a = b) (b = c) H1))
+                    (Conjunct1::explicit (eq::explicit N a b) (eq::explicit N b c) H1)
+                    (Conjunct2::explicit (eq::explicit N a b) (eq::explicit N b c) H1))
                (Refl::explicit N b))
-        (λ H1 : a = d ∧ d = c,
+        (λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
            CongrH::explicit
                a
                b
@@ -51,18 +58,22 @@ Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
                     a
                     d
                     c
-                    (Conjunct1::explicit (a = d) (d = c) H1)
-                    (Conjunct2::explicit (a = d) (d = c) H1))
+                    (Conjunct1::explicit (eq::explicit N a d) (eq::explicit N d c) H1)
+                    (Conjunct2::explicit (eq::explicit N a d) (eq::explicit N d c) H1))
                (Refl::explicit N b))
   Proved: Example2
   Set: 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 : eq::explicit N a b ∧ eq::explicit N b c ∨ eq::explicit N a d ∧ eq::explicit N d c) : eq::explicit
+        N
+        (h a b)
+        (h c b) :=
     DisjCases::explicit
-        (a = b ∧ b = c)
-        (a = d ∧ d = c)
-        ((h a b) = (h c b))
+        (eq::explicit N a b ∧ eq::explicit N b c)
+        (eq::explicit N a d ∧ eq::explicit N d c)
+        ((h a b) == (h c b))
         H
-        (λ H1 : a = b ∧ b = c,
+        (λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
            CongrH::explicit
                a
                b
@@ -73,10 +84,10 @@ Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
                     a
                     b
                     c
-                    (Conjunct1::explicit (a = b) (b = c) H1)
-                    (Conjunct2::explicit (a = b) (b = c) H1))
+                    (Conjunct1::explicit (a == b) (b == c) H1)
+                    (Conjunct2::explicit (a == b) (b == c) H1))
                (Refl::explicit N b))
-        (λ H1 : a = d ∧ d = c,
+        (λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
            CongrH::explicit
                a
                b
@@ -87,8 +98,8 @@ Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
                     a
                     d
                     c
-                    (Conjunct1::explicit (a = d) (d = c) H1)
-                    (Conjunct2::explicit (a = d) (d = c) H1))
+                    (Conjunct1::explicit (a == d) (d == c) H1)
+                    (Conjunct2::explicit (a == d) (d == c) H1))
                (Refl::explicit N b))
   Proved: Example3
   Set: lean::pp::implicit