diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 2c5770bf9..c09f11449 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -77,14 +77,14 @@ theorem trivial : true
 theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
 := H2 H1
 
-theorem eqmp {a b : Bool} (H1 : a == b) (H2 : a) : b
+theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b
 := subst H2 H1
 
 infixl 100 <| : eqmp
 infixl 100 ◂  : eqmp
 
-theorem boolcomplete (a : Bool) : a == true ∨ a == false
-:= case (λ x, x == true ∨ x == false) trivial trivial a
+theorem boolcomplete (a : Bool) : a = true ∨ a = false
+:= case (λ x, x = true ∨ x = false) trivial trivial a
 
 theorem false_elim (a : Bool) (H : false) : a
 := case (λ x, x) trivial H a
@@ -92,14 +92,14 @@ theorem false_elim (a : Bool) (H : false) : a
 theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c
 := assume Ha, H2 (H1 Ha)
 
-theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b == c) : a → c
+theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c
 := assume Ha, H2 ◂ (H1 Ha)
 
-theorem eq_imp_trans {a b c : Bool} (H1 : a == b) (H2 : b → c) : a → c
+theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c
 := assume Ha, H2 (H1 ◂ Ha)
 
-theorem not_not_eq (a : Bool) : (¬ ¬ a) == a
-:= case (λ x, (¬ ¬ x) == x) trivial trivial a
+theorem not_not_eq (a : Bool) : (¬ ¬ a) = a
+:= case (λ x, (¬ ¬ x) = x) trivial trivial a
 
 theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a
 := (not_not_eq a) ◂ H
@@ -169,10 +169,10 @@ theorem eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠
 theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c
 := subst H1 H2
 
-theorem eqt_elim {a : Bool} (H : a == true) : a
+theorem eqt_elim {a : Bool} (H : a = true) : a
 := (symm H) ◂ trivial
 
-theorem eqf_elim {a : Bool} (H : a == false) : ¬ a
+theorem eqf_elim {a : Bool} (H : a = false) : ¬ a
 := not_intro (λ Ha : a, H ◂ Ha)
 
 theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f == g) : f a == g a
@@ -194,31 +194,31 @@ theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
 := assume H1 : (∀ x : A, ¬ P x),
       absurd H (H1 a)
 
-theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a == b
+theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
 := or_elim (boolcomplete a)
-       (λ Hat : a == true,  or_elim (boolcomplete b)
-           (λ Hbt : b == true,  trans Hat (symm Hbt))
-           (λ Hbf : b == false, false_elim (a == b) (subst (Hab (eqt_elim Hat)) Hbf)))
-       (λ Haf : a == false, or_elim (boolcomplete b)
-           (λ Hbt : b == true,  false_elim (a == b) (subst (Hba (eqt_elim Hbt)) Haf))
-           (λ Hbf : b == false, trans Haf (symm Hbf)))
+       (λ Hat : a = true,  or_elim (boolcomplete b)
+           (λ Hbt : b = true,  trans Hat (symm Hbt))
+           (λ Hbf : b = false, false_elim (a = b) (subst (Hab (eqt_elim Hat)) Hbf)))
+       (λ Haf : a = false, or_elim (boolcomplete b)
+           (λ Hbt : b = true,  false_elim (a = b) (subst (Hba (eqt_elim Hbt)) Haf))
+           (λ Hbf : b = false, trans Haf (symm Hbf)))
 
-theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a == b
+theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
 := boolext Hab Hba
 
-theorem eqt_intro {a : Bool} (H : a) : a == true
+theorem eqt_intro {a : Bool} (H : a) : a = true
 := boolext (assume H1 : a,    trivial)
            (assume H2 : true, H)
 
-theorem eqf_intro {a : Bool} (H : ¬ a) : a == false
+theorem eqf_intro {a : Bool} (H : ¬ a) : a = false
 := boolext (assume H1 : a,     absurd H1 H)
            (assume H2 : false, false_elim a H2)
 
-theorem or_comm (a b : Bool) : (a ∨ b) == (b ∨ a)
+theorem or_comm (a b : Bool) : (a ∨ b) = (b ∨ a)
 := boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a))
            (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b))
 
-theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c))
+theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) = (a ∨ (b ∨ c))
 := boolext (assume H : (a ∨ b) ∨ c,
                       or_elim H (λ H1 : a ∨ b, or_elim H1 (λ Ha : a, or_introl Ha (b ∨ c))
                                                           (λ Hb : b, or_intror a (or_introl Hb c)))
@@ -228,118 +228,118 @@ theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c))
                                 (λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c)
                                                           (λ Hc : c, or_intror (a ∨ b) Hc)))
 
-theorem or_id (a : Bool) : (a ∨ a) == a
+theorem or_id (a : Bool) : (a ∨ a) = a
 := boolext (assume H, or_elim H (λ H1, H1) (λ H2, H2))
            (assume H, or_introl H a)
 
-theorem or_falsel (a : Bool) : (a ∨ false) == a
+theorem or_falsel (a : Bool) : (a ∨ false) = a
 := boolext (assume H, or_elim H (λ H1, H1) (λ H2, false_elim a H2))
            (assume H, or_introl H false)
 
-theorem or_falser (a : Bool) : (false ∨ a) == a
+theorem or_falser (a : Bool) : (false ∨ a) = a
 := (or_comm false a) ⋈ (or_falsel a)
 
-theorem or_truel (a : Bool) : (true ∨ a) == true
+theorem or_truel (a : Bool) : (true ∨ a) = true
 := eqt_intro (case (λ x : Bool, true ∨ x) trivial trivial a)
 
-theorem or_truer (a : Bool) : (a ∨ true) == true
+theorem or_truer (a : Bool) : (a ∨ true) = true
 := (or_comm a true) ⋈ (or_truel a)
 
-theorem or_tauto (a : Bool) : (a ∨ ¬ a) == true
+theorem or_tauto (a : Bool) : (a ∨ ¬ a) = true
 := eqt_intro (em a)
 
-theorem and_comm (a b : Bool) : (a ∧ b) == (b ∧ a)
+theorem and_comm (a b : Bool) : (a ∧ b) = (b ∧ a)
 := boolext (assume H, and_intro (and_elimr H) (and_eliml H))
            (assume H, and_intro (and_elimr H) (and_eliml H))
 
-theorem and_id (a : Bool) : (a ∧ a) == a
+theorem and_id (a : Bool) : (a ∧ a) = a
 := boolext (assume H, and_eliml H)
            (assume H, and_intro H H)
 
-theorem and_assoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c))
+theorem and_assoc (a b c : Bool) : ((a ∧ b) ∧ c) = (a ∧ (b ∧ c))
 := boolext (assume H, and_intro (and_eliml (and_eliml H)) (and_intro (and_elimr (and_eliml H)) (and_elimr H)))
            (assume H, and_intro (and_intro (and_eliml H) (and_eliml (and_elimr H))) (and_elimr (and_elimr H)))
 
-theorem and_truer (a : Bool) : (a ∧ true) == a
+theorem and_truer (a : Bool) : (a ∧ true) = a
 := boolext (assume H : a ∧ true,  and_eliml H)
            (assume H : a,         and_intro H trivial)
 
-theorem and_truel (a : Bool) : (true ∧ a) == a
+theorem and_truel (a : Bool) : (true ∧ a) = a
 := trans (and_comm true a) (and_truer a)
 
-theorem and_falsel (a : Bool) : (a ∧ false) == false
+theorem and_falsel (a : Bool) : (a ∧ false) = false
 := boolext (assume H, and_elimr H)
            (assume H, false_elim (a ∧ false) H)
 
-theorem and_falser (a : Bool) : (false ∧ a) == false
+theorem and_falser (a : Bool) : (false ∧ a) = false
 := (and_comm false a) ⋈ (and_falsel a)
 
-theorem and_absurd (a : Bool) : (a ∧ ¬ a) == false
+theorem and_absurd (a : Bool) : (a ∧ ¬ a) = false
 := boolext (assume H, absurd (and_eliml H) (and_elimr H))
            (assume H, false_elim (a ∧ ¬ a) H)
 
-theorem imp_truer (a : Bool) : (a → true) == true
-:= case (λ x, (x → true) == true) trivial trivial a
+theorem imp_truer (a : Bool) : (a → true) = true
+:= case (λ x, (x → true) = true) trivial trivial a
 
-theorem imp_truel (a : Bool) : (true → a) == a
-:= case (λ x, (true → x) == x) trivial trivial a
+theorem imp_truel (a : Bool) : (true → a) = a
+:= case (λ x, (true → x) = x) trivial trivial a
 
-theorem imp_falser (a : Bool) : (a → false) == ¬ a
+theorem imp_falser (a : Bool) : (a → false) = ¬ a
 := refl _
 
-theorem imp_falsel (a : Bool) : (false → a) == true
-:= case (λ x, (false → x) == true) trivial trivial a
+theorem imp_falsel (a : Bool) : (false → a) = true
+:= case (λ x, (false → x) = true) trivial trivial a
 
-theorem not_and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b)
-:= case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b))
-        (case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y))   trivial trivial b)
-        (case (λ y, (¬ (false ∧ y)) == (¬ false ∨ ¬ y)) trivial trivial b)
+theorem not_and (a b : Bool) : (¬ (a ∧ b)) = (¬ a ∨ ¬ b)
+:= case (λ x, (¬ (x ∧ b)) = (¬ x ∨ ¬ b))
+        (case (λ y, (¬ (true ∧ y)) = (¬ true ∨ ¬ y))   trivial trivial b)
+        (case (λ y, (¬ (false ∧ y)) = (¬ false ∨ ¬ y)) trivial trivial b)
         a
 
 theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
 := (not_and a b) ◂ H
 
-theorem not_or (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b)
-:= case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b))
-        (case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y))   trivial trivial b)
-        (case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) trivial trivial b)
+theorem not_or (a b : Bool) : (¬ (a ∨ b)) = (¬ a ∧ ¬ b)
+:= case (λ x, (¬ (x ∨ b)) = (¬ x ∧ ¬ b))
+        (case (λ y, (¬ (true ∨ y)) = (¬ true ∧ ¬ y))   trivial trivial b)
+        (case (λ y, (¬ (false ∨ y)) = (¬ false ∧ ¬ y)) trivial trivial b)
         a
 
 theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
 := (not_or a b) ◂ H
 
-theorem not_iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b)
-:= case (λ x, (¬ (x == b)) == ((¬ x) == b))
-        (case (λ y, (¬ (true == y)) == ((¬ true) == y)) trivial trivial b)
-        (case (λ y, (¬ (false == y)) == ((¬ false) == y)) trivial trivial b)
+theorem not_iff (a b : Bool) : (¬ (a = b)) = ((¬ a) = b)
+:= case (λ x, (¬ (x = b)) = ((¬ x) = b))
+        (case (λ y, (¬ (true = y)) = ((¬ true) = y)) trivial trivial b)
+        (case (λ y, (¬ (false = y)) = ((¬ false) = y)) trivial trivial b)
         a
 
-theorem not_iff_elim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b
+theorem not_iff_elim {a b : Bool} (H : ¬ (a = b)) : (¬ a) = b
 := (not_iff a b) ◂ H
 
-theorem not_implies (a b : Bool) : (¬ (a → b)) == (a ∧ ¬ b)
-:= case (λ x, (¬ (x → b)) == (x ∧ ¬ b))
-        (case (λ y, (¬ (true → y)) == (true ∧ ¬ y)) trivial trivial b)
-        (case (λ y, (¬ (false → y)) == (false ∧ ¬ y)) trivial trivial b)
+theorem not_implies (a b : Bool) : (¬ (a → b)) = (a ∧ ¬ b)
+:= case (λ x, (¬ (x → b)) = (x ∧ ¬ b))
+        (case (λ y, (¬ (true → y)) = (true ∧ ¬ y)) trivial trivial b)
+        (case (λ y, (¬ (false → y)) = (false ∧ ¬ y)) trivial trivial b)
         a
 
 theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
 := (not_implies a b) ◂ H
 
-theorem not_congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b)
+theorem not_congr {a b : Bool} (H : a = b) : (¬ a) = (¬ b)
 := congr2 not H
 
-theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x)
+theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x = Q x) : (∃ x : A, P x) = (∃ x : A, Q x)
 := congr2 (Exists A) (funext H)
 
-theorem not_forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x)
+theorem not_forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) = (∃ x : A, ¬ P x)
 := calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not_congr (allext (λ x : A, symm (not_not_eq (P x))))
               ...        = (∃ x : A, ¬ P x)     : refl (∃ x : A, ¬ P x)
 
 theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
 := (not_forall A P) ◂ H
 
-theorem not_exists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x)
+theorem not_exists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) = (∀ x : A, ¬ P x)
 := calc (¬ ∃ x : A, P x) = (¬ ¬ ∀ x : A, ¬ P x) : refl (¬ ∃ x : A, P x)
                      ... = (∀ x : A, ¬ P x)     : not_not_eq (∀ x : A, ¬ P x)
 
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 4e34ee73e..8bf6de6fd 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp
index e7d957a0b..18ee9fecc 100644
--- a/src/library/simplifier/ceq.cpp
+++ b/src/library/simplifier/ceq.cpp
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "library/expr_pair.h"
 #include "library/ite.h"
 #include "library/kernel_bindings.h"
-#include "library/eq_heq.h"
 
 namespace lean {
 static name g_Hc("Hc"); // auxiliary name for if-then-else
@@ -45,11 +44,11 @@ class to_ceqs_fn {
     }
 
     list<expr_pair> apply(expr const & e, expr const & H) {
-        if (is_eq(e) || is_heq(e)) {
+        if (is_eq(e)) {
             return mk_singleton(e, H);
         } else if (is_not(e)) {
             expr a     = arg(e, 1);
-            expr new_e = mk_heq(a, False);
+            expr new_e = mk_eq(Bool, a, False);
             expr new_H = mk_eqf_intro_th(a, H);
             return mk_singleton(new_e, new_H);
         } else if (is_and(e)) {
@@ -93,7 +92,7 @@ class to_ceqs_fn {
                 });
             return append(new_then_ceqs, new_else_ceqs);
         } else {
-            return mk_singleton(mk_heq(e, True), mk_eqt_intro_th(e, H));
+            return mk_singleton(mk_eq(Bool, e, True), mk_eqt_intro_th(e, H));
         }
     }
 public:
@@ -118,10 +117,10 @@ bool is_ceq(ro_environment const & env, expr e) {
         ctx = extend(ctx, abst_name(e), abst_domain(e));
         e = abst_body(e);
     }
-    if (is_eq_heq(e)) {
-        auto lhs_rhs = eq_heq_args(e);
+    if (is_eq(e)) {
+        expr lhs = arg(e, 2);
         // traverse lhs, and mark all variables that occur there in is_lhs.
-        for_each(lhs_rhs.first, [&](expr const & e, unsigned offset) {
+        for_each(lhs, [&](expr const & e, unsigned offset) {
                 if (is_var(e)) {
                     unsigned vidx = var_idx(e);
                     if (vidx >= offset) {