diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 683de6c19..3e1db1ada 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,4 +1,4 @@
-add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp
+add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
 # free_vars.cpp abstract.cpp instantiate.cpp
 # normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
 # type_checker.cpp kernel.cpp occurs.cpp metavar.cpp
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 51ed6a387..561970ce1 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -9,35 +9,33 @@ Author: Leonardo de Moura
 #include <sstream>
 #include <string>
 #include <algorithm>
+#include "util/list_fn.h"
 #include "util/hash.h"
 #include "util/buffer.h"
 #include "util/object_serializer.h"
 #include "kernel/expr.h"
+#include "kernel/expr_eq_fn.h"
 // #include "kernel/free_vars.h"
-// #include "kernel/expr_eq.h"
 // #include "kernel/metavar.h"
 // #include "kernel/max_sharing.h"
 
 namespace lean {
-#if 0
 static expr g_dummy(mk_var(0));
 expr::expr():expr(g_dummy) {}
 
-// Local context entries
-local_entry::local_entry(unsigned s, unsigned n):m_kind(local_entry_kind::Lift), m_s(s), m_n(n) {}
-local_entry::local_entry(unsigned s, expr const & v):m_kind(local_entry_kind::Inst), m_s(s), m_v(v) {}
-local_entry::~local_entry() {}
-bool local_entry::operator==(local_entry const & e) const {
-    if (m_kind != e.m_kind || m_s != e.m_s)
-        return false;
-    if (is_inst())
-        return m_v == e.m_v;
-    else
-        return m_n == e.m_n;
+unsigned hash_levels(levels const & ls) {
+    unsigned r = 23;
+    for (auto const & l : ls)
+        r = hash(hash(l), r);
+    return r;
 }
 
-unsigned hash_args(unsigned size, expr const * args) {
-    return hash(size, [&args](unsigned i){ return args[i].hash(); });
+bool has_meta(levels const & ls) {
+    for (auto const & l : ls) {
+        if (has_meta(l))
+            return true;
+    }
+    return false;
 }
 
 expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv):
@@ -46,7 +44,7 @@ expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv):
     m_hash(h),
     m_rc(0) {
     // m_hash_alloc does not need to be a unique identifier.
-    // We want diverse hash codes such that given expr_cell * c1 and expr_cell * c2,
+    // We want diverse hash codes because given expr_cell * c1 and expr_cell * c2,
     // if c1 != c2, then there is high probability c1->m_hash_alloc != c2->m_hash_alloc.
     // Remark: using pointer address as a hash code is not a good idea.
     //    - each execution run will behave differently.
@@ -95,30 +93,31 @@ expr_var::expr_var(unsigned idx):
     m_vidx(idx) {}
 
 // Expr constants
-expr_const::expr_const(name const & n, optional<expr> const & t):
-    expr_cell(expr_kind::Constant, n.hash(), t && t->has_metavar()),
+expr_const::expr_const(name const & n, levels const & ls):
+    expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), has_meta(ls)),
+    m_name(n),
+    m_levels(ls) {}
+
+// Expr metavariables and local variables
+expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t):
+    expr_cell(is_meta ? expr_kind::Meta : expr_kind::Local, n.hash(), t.has_metavar()),
     m_name(n),
     m_type(t) {}
-void expr_const::dealloc(buffer<expr_cell*> & todelete) {
+void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_type, todelete);
     delete(this);
 }
 
-// Expr heterogeneous equality
-expr_heq::expr_heq(expr const & lhs, expr const & rhs):
-    expr_cell(expr_kind::HEq, ::lean::hash(lhs.hash(), rhs.hash()), lhs.has_metavar() || rhs.has_metavar()),
-    m_lhs(lhs), m_rhs(rhs), m_depth(std::max(get_depth(lhs), get_depth(rhs))+1) {
-}
-void expr_heq::dealloc(buffer<expr_cell*> & todelete) {
-    dec_ref(m_lhs, todelete);
-    dec_ref(m_rhs, todelete);
-    delete(this);
-}
+// Composite expressions
+expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, unsigned d):
+    expr_cell(k, h, has_mv),
+    m_depth(d) {}
 
 // Expr dependent pairs
 expr_dep_pair::expr_dep_pair(expr const & f, expr const & s, expr const & t):
-    expr_cell(expr_kind::Pair, ::lean::hash(f.hash(), s.hash()), f.has_metavar() || s.has_metavar() || t.has_metavar()),
-    m_first(f), m_second(s), m_type(t), m_depth(std::max(get_depth(f), get_depth(s))+1) {
+    expr_composite(expr_kind::Pair, ::lean::hash(f.hash(), s.hash()), f.has_metavar() || s.has_metavar() || t.has_metavar(),
+                   std::max(get_depth(f), get_depth(s))+1),
+    m_first(f), m_second(s), m_type(t) {
 }
 void expr_dep_pair::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_first,  todelete);
@@ -129,100 +128,54 @@ void expr_dep_pair::dealloc(buffer<expr_cell*> & todelete) {
 
 // Expr pair projection
 expr_proj::expr_proj(bool f, expr const & e):
-    expr_cell(expr_kind::Proj, ::lean::hash(17, e.hash()), e.has_metavar()),
-    m_first(f), m_depth(get_depth(e)+1), m_expr(e) {}
+    expr_composite(f ? expr_kind::Fst : expr_kind::Snd, ::lean::hash(17, e.hash()), e.has_metavar(), get_depth(e)+1),
+    m_expr(e) {}
 void expr_proj::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_expr, todelete);
     delete(this);
 }
 
 // Expr applications
-expr_app::expr_app(unsigned num_args, bool has_mv):
-    expr_cell(expr_kind::App, 0, has_mv),
-    m_num_args(num_args) {
-}
+expr_app::expr_app(expr const & fn, expr const & arg):
+    expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()), fn.has_metavar() || arg.has_metavar(),
+                   std::max(get_depth(fn), get_depth(arg)) + 1),
+    m_fn(fn), m_arg(arg) {}
 void expr_app::dealloc(buffer<expr_cell*> & todelete) {
-    unsigned i = m_num_args;
-    while (i > 0) {
-        --i;
-        dec_ref(m_args[i], todelete);
-    }
-    delete[] reinterpret_cast<char*>(this);
-}
-expr mk_app(unsigned n, expr const * as) {
-    lean_assert(n > 1);
-    unsigned new_n;
-    unsigned n0 = 0;
-    expr const & arg0 = as[0];
-    bool has_mv = std::any_of(as, as + n, [](expr const & c) { return c.has_metavar(); });
-    // Remark: we represent ((app a b) c) as (app a b c)
-    if (is_app(arg0)) {
-        n0    = num_args(arg0);
-        new_n = n + n0 - 1;
-    } else {
-        new_n = n;
-    }
-    char * mem   = new char[sizeof(expr_app) + new_n*sizeof(expr)];
-    expr r(new (mem) expr_app(new_n, has_mv));
-    expr * m_args = to_app(r)->m_args;
-    unsigned i = 0;
-    unsigned j = 0;
-    unsigned depth = 0;
-    if (new_n != n) {
-        for (; i < n0; ++i) {
-            new (m_args+i) expr(arg(arg0, i));
-            depth = std::max(depth, get_depth(m_args[i]));
-        }
-        j++;
-    }
-    for (; i < new_n; ++i, ++j) {
-        lean_assert(j < n);
-        new (m_args+i) expr(as[j]);
-        depth = std::max(depth, get_depth(m_args[i]));
-    }
-    to_app(r)->m_hash  = hash_args(new_n, m_args);
-    to_app(r)->m_depth = depth + 1;
-    return r;
+    dec_ref(m_fn, todelete);
+    dec_ref(m_arg, todelete);
+    delete(this);
 }
 
-// Expr abstractions (and subclasses: Lambda, Pi and Sigma)
-expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b):
-    expr_cell(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar()),
+// Expr binders (Lambda, Pi and Sigma)
+expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b):
+    expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar(),
+                   std::max(get_depth(m_domain), get_depth(m_body)) + 1),
     m_name(n),
     m_domain(t),
     m_body(b) {
-    m_depth = 1 + std::max(get_depth(m_domain), get_depth(m_body));
+    lean_assert(k == expr_kind::Lambda || k == expr_kind::Pi || k == expr_kind::Sigma);
 }
-void expr_abstraction::dealloc(buffer<expr_cell*> & todelete) {
+void expr_binder::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_body, todelete);
     dec_ref(m_domain, todelete);
     delete(this);
 }
 
-expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Lambda, n, t, e) {}
-
-expr_pi::expr_pi(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Pi, n, t, e) {}
-
-expr_sigma::expr_sigma(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Sigma, n, t, e) {}
-
-// Expr Type
-expr_type::expr_type(level const & l):
-    expr_cell(expr_kind::Type, l.hash(), false),
+// Expr Sort
+expr_sort::expr_sort(level const & l):
+    expr_cell(expr_kind::Sort, ::lean::hash(l), has_meta(l)),
     m_level(l) {
 }
-expr_type::~expr_type() {}
+expr_sort::~expr_sort() {}
 
 // Expr Let
 expr_let::expr_let(name const & n, optional<expr> const & t, expr const & v, expr const & b):
-    expr_cell(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), v.has_metavar() || b.has_metavar() || (t && t->has_metavar())),
+    expr_composite(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), v.has_metavar() || b.has_metavar() || ::lean::has_metavar(t),
+                   std::max({get_depth(t), get_depth(v), get_depth(b)}) + 1),
     m_name(n),
     m_type(t),
     m_value(v),
     m_body(b) {
-    unsigned depth = std::max(get_depth(m_value), get_depth(m_body));
-    if (m_type)
-        depth = std::max(depth, get_depth(*m_type));
-    m_depth = 1 + depth;
 }
 void expr_let::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_body, todelete);
@@ -232,55 +185,49 @@ void expr_let::dealloc(buffer<expr_cell*> & todelete) {
 }
 expr_let::~expr_let() {}
 
-// Expr Semantic attachment
-name value::get_unicode_name() const { return get_name(); }
-optional<expr> value::normalize(unsigned, expr const *) const { return none_expr(); }
-void value::display(std::ostream & out) const { out << get_name(); }
-bool value::operator==(value const & other) const { return typeid(*this) == typeid(other); }
-bool value::operator<(value const & other) const {
+// Macro attachment
+int macro::push_lua(lua_State *) const { return 0; } // NOLINT
+void macro::display(std::ostream & out) const { out << get_name(); }
+bool macro::operator==(macro const & other) const { return typeid(*this) == typeid(other); }
+bool macro::operator<(macro const & other) const {
     if (get_name() == other.get_name())
         return lt(other);
     else
         return get_name() < other.get_name();
 }
-format value::pp() const { return format(get_name()); }
-format value::pp(bool unicode, bool) const { return unicode ? format(get_unicode_name()) : pp(); }
-unsigned value::hash() const { return get_name().hash(); }
-int value::push_lua(lua_State *) const { return 0; } // NOLINT
-expr_value::expr_value(value & v):
-    expr_cell(expr_kind::Value, v.hash(), false),
-    m_val(v) {
-    m_val.inc_ref();
-}
-expr_value::~expr_value() {
-    m_val.dec_ref();
-}
-typedef std::unordered_map<std::string, value::reader> value_readers;
-static std::unique_ptr<value_readers> g_value_readers;
-value_readers & get_value_readers() {
-    if (!g_value_readers)
-        g_value_readers.reset(new value_readers());
-    return *(g_value_readers.get());
+format macro::pp(formatter const &, options const &) const { return format(get_name()); }
+bool macro::is_atomic_pp(bool, bool) const { return true; }
+unsigned macro::hash() const { return get_name().hash(); }
+
+typedef std::unordered_map<std::string, macro::reader> macro_readers;
+static std::unique_ptr<macro_readers> g_macro_readers;
+macro_readers & get_macro_readers() {
+    if (!g_macro_readers)
+        g_macro_readers.reset(new macro_readers());
+    return *(g_macro_readers.get());
 }
 
-void value::register_deserializer(std::string const & k, value::reader rd) {
-    value_readers & readers = get_value_readers();
+void macro::register_deserializer(std::string const & k, macro::reader rd) {
+    macro_readers & readers = get_macro_readers();
     lean_assert(readers.find(k) == readers.end());
     readers[k] = rd;
 }
-static expr read_value(deserializer & d) {
+static expr read_macro(deserializer & d) {
     auto k  = d.read_string();
-    value_readers & readers = get_value_readers();
+    macro_readers & readers = get_macro_readers();
     auto it = readers.find(k);
     lean_assert(it != readers.end());
     return it->second(d);
 }
 
-// Expr Metavariable
-expr_metavar::expr_metavar(name const & n, local_context const & lctx):
-    expr_cell(expr_kind::MetaVar, n.hash(), true),
-    m_name(n), m_lctx(lctx) {}
-expr_metavar::~expr_metavar() {}
+expr_macro::expr_macro(macro * m):
+    expr_cell(expr_kind::Macro, m->hash(), false),
+    m_macro(m) {
+    m_macro->inc_ref();
+}
+expr_macro::~expr_macro() {
+    m_macro->dec_ref();
+}
 
 void expr_cell::dealloc() {
     try {
@@ -292,17 +239,18 @@ void expr_cell::dealloc() {
             lean_assert(it->get_rc() == 0);
             switch (it->kind()) {
             case expr_kind::Var:        delete static_cast<expr_var*>(it); break;
-            case expr_kind::Value:      delete static_cast<expr_value*>(it); break;
-            case expr_kind::MetaVar:    delete static_cast<expr_metavar*>(it); break;
-            case expr_kind::Type:       delete static_cast<expr_type*>(it); break;
-            case expr_kind::Constant:   static_cast<expr_const*>(it)->dealloc(todo); break;
+            case expr_kind::Macro:      delete static_cast<expr_macro*>(it); break;
+            case expr_kind::Meta:
+            case expr_kind::Local:      static_cast<expr_mlocal*>(it)->dealloc(todo); break;
+            case expr_kind::Constant:   delete static_cast<expr_const*>(it); break;
+            case expr_kind::Sort:       delete static_cast<expr_sort*>(it); break;
             case expr_kind::Pair:       static_cast<expr_dep_pair*>(it)->dealloc(todo); break;
-            case expr_kind::Proj:       static_cast<expr_proj*>(it)->dealloc(todo); break;
+            case expr_kind::Fst:
+            case expr_kind::Snd:        static_cast<expr_proj*>(it)->dealloc(todo); break;
             case expr_kind::App:        static_cast<expr_app*>(it)->dealloc(todo); break;
-            case expr_kind::Lambda:     static_cast<expr_lambda*>(it)->dealloc(todo); break;
-            case expr_kind::Pi:         static_cast<expr_pi*>(it)->dealloc(todo); break;
-            case expr_kind::Sigma:      static_cast<expr_sigma*>(it)->dealloc(todo); break;
-            case expr_kind::HEq:        static_cast<expr_heq*>(it)->dealloc(todo); break;
+            case expr_kind::Lambda:
+            case expr_kind::Pi:
+            case expr_kind::Sigma:      static_cast<expr_binder*>(it)->dealloc(todo); break;
             case expr_kind::Let:        static_cast<expr_let*>(it)->dealloc(todo); break;
             }
         }
@@ -312,15 +260,44 @@ void expr_cell::dealloc() {
     }
 }
 
-expr mk_type() {
-    static LEAN_THREAD_LOCAL expr r = mk_type(level());
+// Auxiliary constructors
+expr mk_app(unsigned num_args, expr const * args) {
+    lean_assert(num_args >= 2);
+    expr r = mk_app(args[0], args[1]);
+    for (unsigned i = 2; i < num_args; i++)
+        r = mk_app(r, args[i]);
     return r;
 }
 
-bool operator==(expr const & a, expr const & b) {
-    return expr_eq_fn<>()(a, b);
+static name g_default_var_name("a");
+bool is_default_var_name(name const & n) { return n == g_default_var_name; }
+expr mk_arrow(expr const & t, expr const & e) { return mk_pi(g_default_var_name, t, e); }
+expr mk_cartesian_product(expr const & t, expr const & e) { return mk_sigma(g_default_var_name, t, e); }
+
+expr Bool = mk_sort(mk_level_zero());
+expr Type = mk_sort(mk_level_one());
+expr mk_Bool() { return Bool; }
+expr mk_Type() { return Type; }
+
+unsigned get_depth(expr const & e) {
+    switch (e.kind()) {
+    case expr_kind::Var:  case expr_kind::Constant: case expr_kind::Sort:
+    case expr_kind::Meta: case expr_kind::Local:    case expr_kind::Macro:
+        return 1;
+    case expr_kind::Lambda: case expr_kind::Pi:   case expr_kind::Sigma:
+    case expr_kind::Pair:   case expr_kind::Fst:  case expr_kind::Snd:
+    case expr_kind::App:    case expr_kind::Let:
+        return static_cast<expr_composite*>(e.raw())->m_depth;
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
+bool operator==(expr const & a, expr const & b) { return expr_eq_fn()(a, b); }
+
+#if 0
+
+
+
 bool is_arrow(expr const & t) {
     optional<bool> r = t.raw()->is_arrow();
     if (r) {
@@ -336,26 +313,6 @@ bool is_cartesian(expr const & t) {
     return is_sigma(t) && !has_free_var(abst_body(t), 0);
 }
 
-unsigned get_depth(expr const & e) {
-    switch (e.kind()) {
-    case expr_kind::Var:   case expr_kind::Constant:  case expr_kind::Type:
-    case expr_kind::Value: case expr_kind::MetaVar:
-        return 1;
-    case expr_kind::HEq:
-        return to_heq(e)->m_depth;
-    case expr_kind::Pair:
-        return to_pair(e)->m_depth;
-    case expr_kind::Proj:
-        return to_proj(e)->m_depth;
-    case expr_kind::App:
-        return to_app(e)->m_depth;
-    case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Sigma:
-        return to_abstraction(e)->m_depth;
-    case expr_kind::Let:
-        return to_let(e)->m_depth;
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
 
 expr copy(expr const & a) {
     switch (a.kind()) {
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 51d20c0da..d579197dc 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -25,6 +25,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 class expr;
+typedef list<level> levels;
 /* =======================================
    Expressions
    expr ::=   Var           idx
@@ -120,7 +121,7 @@ public:
 
     friend expr mk_var(unsigned idx);
     friend expr mk_sort(level const & l);
-    friend expr mk_constant(name const & n, list<level> const & ls);
+    friend expr mk_constant(name const & n, levels const & ls);
     friend expr mk_metavar(name const & n, expr const & t);
     friend expr mk_local(name const & n, expr const & t);
     friend expr mk_app(expr const & f, expr const & a);
@@ -173,22 +174,22 @@ public:
 
 /** \brief (parametric) Constants. */
 class expr_const : public expr_cell {
-    name           m_name;
-    list<level>    m_levels;
-    friend class expr_cell;
-    void dealloc(buffer<expr_cell*> & to_delete);
+    name       m_name;
+    levels     m_levels;
 public:
-    expr_const(name const & n, list<level> const & ls);
+    expr_const(name const & n, levels const & ls);
     name const & get_name() const { return m_name; }
-    list<level> const & get_level_params() const { return m_levels; }
+    levels const & get_level_params() const { return m_levels; }
 };
 
 /** \brief Metavariables and local constants */
-class expr_meta_local : public expr_cell {
+class expr_mlocal : public expr_cell {
     name   m_name;
     expr   m_type;
+    friend expr_cell;
+    void dealloc(buffer<expr_cell*> & todelete);
 public:
-    expr_meta_local(bool is_meta, name const & n, expr const & t);
+    expr_mlocal(bool is_meta, name const & n, expr const & t);
     name const & get_name() const { return m_name; }
     expr const & get_type() const { return m_type; }
 };
@@ -218,8 +219,8 @@ class expr_dep_pair : public expr_composite {
     expr     m_first;
     expr     m_second;
     expr     m_type;
-    friend expr_cell;
     friend expr mk_pair(expr const & f, expr const & s, expr const & t);
+    friend expr_cell;
     void dealloc(buffer<expr_cell*> & todelete);
 public:
     expr_dep_pair(expr const & f, expr const & s, expr const & t);
@@ -343,7 +344,7 @@ inline bool is_sort(expr_cell * e)        { return e->kind() == expr_kind::Sort;
 inline bool is_let(expr_cell * e)         { return e->kind() == expr_kind::Let; }
 inline bool is_binder(expr_cell * e)      { return is_lambda(e) || is_pi(e) || is_sigma(e); }
 inline bool is_proj(expr_cell * e)        { return is_fst(e) || is_snd(e); }
-inline bool is_meta_local(expr_cell * e)  { return is_metavar(e) || is_local(e); }
+inline bool is_mlocal(expr_cell * e)      { return is_metavar(e) || is_local(e); }
 
 inline bool is_var(expr const & e)        { return e.kind() == expr_kind::Var; }
 inline bool is_constant(expr const & e)   { return e.kind() == expr_kind::Constant; }
@@ -361,19 +362,19 @@ inline bool is_sort(expr const & e)       { return e.kind() == expr_kind::Sort;
 inline bool is_let(expr const & e)        { return e.kind() == expr_kind::Let; }
 inline bool is_binder(expr const & e)     { return is_lambda(e) || is_pi(e) || is_sigma(e); }
 inline bool is_proj(expr const & e)       { return is_fst(e) || is_snd(e); }
-inline bool is_meta_local(expr const & e) { return is_metavar(e) || is_local(e); }
+inline bool is_mlocal(expr const & e)     { return is_metavar(e) || is_local(e); }
 // =======================================
 
 // =======================================
 // Constructors
 inline expr mk_var(unsigned idx) { return expr(new expr_var(idx)); }
 inline expr Var(unsigned idx) { return mk_var(idx); }
-inline expr mk_constant(name const & n, list<level> const & ls) { return expr(new expr_const(n, ls)); }
-inline expr mk_constant(name const & n) { return mk_constant(n, list<level>()); }
+inline expr mk_constant(name const & n, levels const & ls) { return expr(new expr_const(n, ls)); }
+inline expr mk_constant(name const & n) { return mk_constant(n, levels()); }
 inline expr Const(name const & n) { return mk_constant(n); }
 inline expr mk_macro(macro * m) { return expr(new expr_macro(m)); }
-inline expr mk_metavar(name const & n, expr const & t) { return expr(new expr_meta_local(true, n, t)); }
-inline expr mk_local(name const & n, expr const & t) { return expr(new expr_meta_local(false, n, t)); }
+inline expr mk_metavar(name const & n, expr const & t) { return expr(new expr_mlocal(true, n, t)); }
+inline expr mk_local(name const & n, expr const & t) { return expr(new expr_mlocal(false, n, t)); }
 inline expr mk_pair(expr const & f, expr const & s, expr const & t) { return expr(new expr_dep_pair(f, s, t)); }
 inline expr mk_fst(expr const & a) { return expr(new expr_proj(true, a)); }
 inline expr mk_snd(expr const & a) { return expr(new expr_proj(false, a)); }
@@ -384,21 +385,23 @@ template<typename T> expr mk_app(T const & args) { return mk_app(args.size(), ar
 inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Lambda, n, t, e)); }
 inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Pi, n, t, e)); }
 inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Sigma, n, t, e)); }
-inline bool is_default_arrow_var_name(name const & n) { return n == "a"; }
-inline expr mk_arrow(expr const & t, expr const & e) { return mk_pi(name("a"), t, e); }
-inline expr mk_cartesian_product(expr const & t, expr const & e) { return mk_sigma(name("a"), t, e); }
-inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); }
 inline expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e) {
     return expr(new expr_let(n, t, v, e));
 }
 inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return mk_let(n, some_expr(t), v, e); }
 inline expr mk_let(name const & n, expr const & v, expr const & e) { return mk_let(n, none_expr(), v, e); }
 inline expr mk_sort(level const & l) { return expr(new expr_sort(l)); }
+
 expr mk_Bool();
 expr mk_Type();
 extern expr Type;
 extern expr Bool;
 
+bool is_default_var_name(name const & n);
+expr mk_arrow(expr const & t, expr const & e);
+expr mk_cartesian_product(expr const & t, expr const & e);
+inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); }
+
 // Auxiliary
 inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); }
 inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); }
@@ -438,9 +441,9 @@ inline expr_app *         to_app(expr_cell * e)        { lean_assert(is_app(e));
 inline expr_binder *      to_binder(expr_cell * e)     { lean_assert(is_binder(e));      return static_cast<expr_binder*>(e); }
 inline expr_let *         to_let(expr_cell * e)        { lean_assert(is_let(e));         return static_cast<expr_let*>(e); }
 inline expr_sort *        to_sort(expr_cell * e)       { lean_assert(is_sort(e));        return static_cast<expr_sort*>(e); }
-inline expr_meta_local *  to_meta_local(expr_cell * e) { lean_assert(is_meta_local(e));  return static_cast<expr_meta_local*>(e); }
-inline expr_meta_local *  to_local(expr_cell * e)      { lean_assert(is_local(e));       return static_cast<expr_meta_local*>(e); }
-inline expr_meta_local *  to_metavar(expr_cell * e)    { lean_assert(is_metavar(e));     return static_cast<expr_meta_local*>(e); }
+inline expr_mlocal *      to_mlocal(expr_cell * e)     { lean_assert(is_mlocal(e));      return static_cast<expr_mlocal*>(e); }
+inline expr_mlocal *      to_local(expr_cell * e)      { lean_assert(is_local(e));       return static_cast<expr_mlocal*>(e); }
+inline expr_mlocal *      to_metavar(expr_cell * e)    { lean_assert(is_metavar(e));     return static_cast<expr_mlocal*>(e); }
 
 inline expr_var *         to_var(expr const & e)         { return to_var(e.raw()); }
 inline expr_const *       to_constant(expr const & e)    { return to_constant(e.raw()); }
@@ -450,88 +453,71 @@ inline expr_app *         to_app(expr const & e)         { return to_app(e.raw()
 inline expr_binder *      to_binder(expr const & e)      { return to_binder(e.raw()); }
 inline expr_let *         to_let(expr const & e)         { return to_let(e.raw()); }
 inline expr_sort *        to_sort(expr const & e)        { return to_sort(e.raw()); }
-inline expr_meta_local *  to_meta_local(expr const & e)  { return to_meta_local(e.raw()); }
-inline expr_meta_local *  to_metavar(expr const & e)     { return to_metavar(e.raw()); }
-inline expr_meta_local *  to_local(expr const & e)       { return to_local(e.raw()); }
+inline expr_mlocal *      to_mlocal(expr const & e)      { return to_mlocal(e.raw()); }
+inline expr_mlocal *      to_metavar(expr const & e)     { return to_metavar(e.raw()); }
+inline expr_mlocal *      to_local(expr const & e)       { return to_local(e.raw()); }
 // =======================================
 
 
-#if 0
-
-
 // =======================================
 // Accessors
-inline unsigned      get_rc(expr_cell * e)               { return e->get_rc(); }
-inline bool          is_shared(expr_cell * e)            { return get_rc(e) > 1; }
-inline unsigned      var_idx(expr_cell * e)              { return to_var(e)->get_vidx(); }
-inline bool          is_var(expr_cell * e, unsigned i)   { return is_var(e) && var_idx(e) == i; }
-inline name const &  const_name(expr_cell * e)           { return to_constant(e)->get_name(); }
-// Remark: the following function should not be exposed in the internal API.
-inline optional<expr> const &  const_type(expr_cell * e) { return to_constant(e)->get_type(); }
-inline expr const &  pair_first(expr_cell * e)           { return to_pair(e)->get_first(); }
-inline expr const &  pair_second(expr_cell * e)          { return to_pair(e)->get_second(); }
-inline expr const &  pair_type(expr_cell * e)            { return to_pair(e)->get_type(); }
-inline bool          proj_first(expr_cell * e)           { return to_proj(e)->first(); }
-inline expr const &  proj_arg(expr_cell * e)             { return to_proj(e)->get_arg(); }
-inline value const & to_value(expr_cell * e)             { lean_assert(is_value(e)); return static_cast<expr_value*>(e)->get_value(); }
-inline unsigned      num_args(expr_cell * e)             { return to_app(e)->get_num_args(); }
-inline expr const &  arg(expr_cell * e, unsigned idx)    { return to_app(e)->get_arg(idx); }
-inline name const &  abst_name(expr_cell * e)            { return to_abstraction(e)->get_name(); }
-inline expr const &  abst_domain(expr_cell * e)          { return to_abstraction(e)->get_domain(); }
-inline expr const &  abst_body(expr_cell * e)            { return to_abstraction(e)->get_body(); }
-inline level const & ty_level(expr_cell * e)             { return to_type(e)->get_level(); }
-inline name const &  let_name(expr_cell * e)             { return to_let(e)->get_name(); }
-inline expr const &  let_value(expr_cell * e)            { return to_let(e)->get_value(); }
-inline optional<expr> const &  let_type(expr_cell * e)   { return to_let(e)->get_type(); }
-inline expr const &  let_body(expr_cell * e)             { return to_let(e)->get_body(); }
-inline expr const &  heq_lhs(expr_cell * e)              { return to_heq(e)->get_lhs(); }
-inline expr const &  heq_rhs(expr_cell * e)              { return to_heq(e)->get_rhs(); }
-inline name const &  metavar_name(expr_cell * e)         { return to_metavar(e)->get_name(); }
-inline local_context const & metavar_lctx(expr_cell * e) { return to_metavar(e)->get_lctx(); }
+inline unsigned       get_rc(expr_cell * e)               { return e->get_rc(); }
+inline bool           is_shared(expr_cell * e)            { return get_rc(e) > 1; }
+inline unsigned       var_idx(expr_cell * e)              { return to_var(e)->get_vidx(); }
+inline bool           is_var(expr_cell * e, unsigned i)   { return is_var(e) && var_idx(e) == i; }
+inline name const &   const_name(expr_cell * e)           { return to_constant(e)->get_name(); }
+inline levels const & const_level_params(expr_cell * e)   { return to_constant(e)->get_level_params(); }
+inline expr const &   pair_first(expr_cell * e)           { return to_pair(e)->get_first(); }
+inline expr const &   pair_second(expr_cell * e)          { return to_pair(e)->get_second(); }
+inline expr const &   pair_type(expr_cell * e)            { return to_pair(e)->get_type(); }
+inline expr const &   proj_arg(expr_cell * e)             { return to_proj(e)->get_arg(); }
+inline macro const &  to_macro(expr_cell * e)             {
+    lean_assert(is_macro(e)); return static_cast<expr_macro*>(e)->get_macro(); }
+inline expr const &   app_fn(expr_cell * e)               { return to_app(e)->get_fn(); }
+inline expr const &   app_arg(expr_cell * e)              { return to_app(e)->get_arg(); }
+inline name const &   binder_name(expr_cell * e)          { return to_binder(e)->get_name(); }
+inline expr const &   binder_domain(expr_cell * e)        { return to_binder(e)->get_domain(); }
+inline expr const &   binder_body(expr_cell * e)          { return to_binder(e)->get_body(); }
+inline level const &  sort_level(expr_cell * e)           { return to_sort(e)->get_level(); }
+inline name const &   let_name(expr_cell * e)             { return to_let(e)->get_name(); }
+inline expr const &   let_value(expr_cell * e)            { return to_let(e)->get_value(); }
+inline optional<expr> const &  let_type(expr_cell * e)    { return to_let(e)->get_type(); }
+inline expr const &   let_body(expr_cell * e)             { return to_let(e)->get_body(); }
+inline name const &   mlocal_name(expr_cell * e)          { return to_mlocal(e)->get_name(); }
+inline expr const &   mlocal_type(expr_cell * e)          { return to_mlocal(e)->get_type(); }
 
-/** \brief Return the reference counter of the given expression. */
-inline unsigned      get_rc(expr const &  e)              { return e.raw()->get_rc(); }
-/** \brief Return true iff the reference counter of the given expression is greater than 1. */
-inline bool          is_shared(expr const & e)            { return get_rc(e) > 1; }
-/** \brief Return the de Bruijn index of the given expression. \pre is_var(e) */
-inline unsigned      var_idx(expr const & e)              { return to_var(e)->get_vidx(); }
-/** \brief Return true iff the given expression is a variable with de Bruijn index equal to \c i. */
-inline bool          is_var(expr const & e, unsigned i)   { return is_var(e) && var_idx(e) == i; }
-inline name const &  const_name(expr const & e)           { return to_constant(e)->get_name(); }
-// Remark: the following function should not be exposed in the internal API.
-inline optional<expr> const &  const_type(expr const & e) { return to_constant(e)->get_type(); }
-/** \brief Return true iff the given expression is a constant with name \c n. */
-inline bool          is_constant(expr const & e, name const & n) {
-    return is_constant(e) && const_name(e) == n;
-}
-inline value const & to_value(expr const & e)             { return to_value(e.raw()); }
-inline expr const &  pair_first(expr const & e)           { return to_pair(e)->get_first(); }
-inline expr const &  pair_second(expr const & e)          { return to_pair(e)->get_second(); }
-inline expr const &  pair_type(expr const & e)            { return to_pair(e)->get_type(); }
-inline bool          proj_first(expr const & e)           { return to_proj(e)->first(); }
-inline expr const &  proj_arg(expr const & e)             { return to_proj(e)->get_arg(); }
-inline unsigned      num_args(expr const & e)             { return to_app(e)->get_num_args(); }
-inline expr const &  arg(expr const & e, unsigned idx)    { return to_app(e)->get_arg(idx); }
-inline expr const *  begin_args(expr const & e)           { return to_app(e)->begin_args(); }
-inline expr const *  end_args(expr const & e)             { return to_app(e)->end_args(); }
-inline name const &  abst_name(expr const & e)            { return to_abstraction(e)->get_name(); }
-inline expr const &  abst_domain(expr const & e)          { return to_abstraction(e)->get_domain(); }
-inline expr const &  abst_body(expr const & e)            { return to_abstraction(e)->get_body(); }
-inline level const & ty_level(expr const & e)             { return to_type(e)->get_level(); }
-inline name const &  let_name(expr const & e)             { return to_let(e)->get_name(); }
-inline optional<expr> const &  let_type(expr const & e)   { return to_let(e)->get_type(); }
-inline expr const &  let_value(expr const & e)            { return to_let(e)->get_value(); }
-inline expr const &  let_body(expr const & e)             { return to_let(e)->get_body(); }
-inline expr const &  heq_lhs(expr const & e)              { return to_heq(e)->get_lhs(); }
-inline expr const &  heq_rhs(expr const & e)              { return to_heq(e)->get_rhs(); }
-inline name const &  metavar_name(expr const & e)         { return to_metavar(e)->get_name(); }
-inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)->get_lctx(); }
-/** \brief Return the depth of the given expression */
-unsigned get_depth(expr const & e);
+inline unsigned       get_rc(expr const & e)               { return e.raw()->get_rc(); }
+inline bool           is_shared(expr const & e)            { return get_rc(e) > 1; }
+inline unsigned       var_idx(expr const & e)              { return to_var(e)->get_vidx(); }
+inline bool           is_var(expr const & e, unsigned i)   { return is_var(e) && var_idx(e) == i; }
+inline name const &   const_name(expr const & e)           { return to_constant(e)->get_name(); }
+inline levels const & const_level_params(expr const & e)   { return to_constant(e)->get_level_params(); }
+inline expr const &   pair_first(expr const & e)           { return to_pair(e)->get_first(); }
+inline expr const &   pair_second(expr const & e)          { return to_pair(e)->get_second(); }
+inline expr const &   pair_type(expr const & e)            { return to_pair(e)->get_type(); }
+inline expr const &   proj_arg(expr const & e)             { return to_proj(e)->get_arg(); }
+inline macro const &  to_macro(expr const & e)             { return to_macro(e.raw()); }
+inline expr const &   app_fn(expr const & e)               { return to_app(e)->get_fn(); }
+inline expr const &   app_arg(expr const & e)              { return to_app(e)->get_arg(); }
+inline name const &   binder_name(expr const & e)          { return to_binder(e)->get_name(); }
+inline expr const &   binder_domain(expr const & e)        { return to_binder(e)->get_domain(); }
+inline expr const &   binder_body(expr const & e)          { return to_binder(e)->get_body(); }
+inline level const &  sort_level(expr const & e)           { return to_sort(e)->get_level(); }
+inline name const &   let_name(expr const & e)             { return to_let(e)->get_name(); }
+inline expr const &   let_value(expr const & e)            { return to_let(e)->get_value(); }
+inline optional<expr> const &  let_type(expr const & e)    { return to_let(e)->get_type(); }
+inline expr const &   let_body(expr const & e)             { return to_let(e)->get_body(); }
+inline name const &   mlocal_name(expr const & e)          { return to_mlocal(e)->get_name(); }
+inline expr const &   mlocal_type(expr const & e)          { return to_mlocal(e)->get_type(); }
 
+inline bool is_constant(expr const & e, name const & n) { return is_constant(e) && const_name(e) == n; }
 inline bool has_metavar(expr const & e) { return e.has_metavar(); }
+inline bool has_metavar(optional<expr> const & e) { return e && has_metavar(*e); }
+unsigned get_depth(expr const & e);
+inline unsigned get_depth(optional<expr> const & e) { return e ? get_depth(*e) : 0; }
 // =======================================
 
+
 // =======================================
 // Expression+Offset
 typedef std::pair<expr, unsigned>       expr_offset;
@@ -565,147 +551,22 @@ struct expr_cell_offset_hash { unsigned operator()(expr_cell_offset const & p) c
 struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, expr_cell_offset const & p2) const { return p1 == p2; } };
 // =======================================
 
-// =======================================
-// Miscellaneous
-/**
-   \brief Wrapper for iterating over application arguments.
-
-   If \c n is an application, it allows us to write
-
-   \code
-   for (expr const & arg : app_args(n)) {
-   ... do something with argument
-   }
-   \endcode
-*/
-struct args {
-    expr const & m_app;
-    args(expr const & a):m_app(a) { lean_assert(is_app(a)); }
-    expr const * begin() const { return &arg(m_app, 0); }
-    expr const * end() const { return begin() + num_args(m_app); }
-};
 /**
    \brief Return a shallow copy of \c e
 */
 expr copy(expr const & e);
-// =======================================
+
 
 // =======================================
 // Update
-template<typename F> expr update_app(expr const & e, F f) {
-    static_assert(std::is_same<typename std::result_of<F(expr const &)>::type, expr>::value,
-                  "update_app: return type of f is not expr");
-    buffer<expr> new_args;
-    bool modified = false;
-    for (expr const & a : args(e)) {
-        new_args.push_back(f(a));
-        if (!is_eqp(a, new_args.back()))
-            modified = true;
-    }
-    if (modified)
-        return mk_app(new_args.size(), new_args.data());
-    else
-        return e;
-}
-template<typename F> expr update_abst(expr const & e, F f) {
-    static_assert(std::is_same<typename std::result_of<F(expr const &, expr const &)>::type,
-                  std::pair<expr, expr>>::value,
-                  "update_abst: return type of f is not pair<expr, expr>");
-    expr const & old_t = abst_domain(e);
-    expr const & old_b = abst_body(e);
-    std::pair<expr, expr> p = f(old_t, old_b);
-    if (!is_eqp(p.first, old_t) || !is_eqp(p.second, old_b)) {
-        name const & n = abst_name(e);
-        switch (e.kind()) {
-        case expr_kind::Pi:     return mk_pi(n, p.first, p.second);
-        case expr_kind::Lambda: return mk_lambda(n, p.first, p.second);
-        case expr_kind::Sigma:  return mk_sigma(n, p.first, p.second);
-        default: lean_unreachable();
-        }
-    } else {
-        return e;
-    }
-}
-template<typename F> expr update_let(expr const & e, F f) {
-    static_assert(std::is_same<typename std::result_of<F(optional<expr> const &, expr const &, expr const &)>::type,
-                  std::tuple<optional<expr>, expr, expr>>::value,
-                  "update_let: return type of f is not tuple<optional<expr>, expr, expr>");
-    optional<expr> const & old_t = let_type(e);
-    expr const & old_v           = let_value(e);
-    expr const & old_b           = let_body(e);
-    std::tuple<optional<expr>, expr, expr> r = f(old_t, old_v, old_b);
-    if (!is_eqp(std::get<0>(r), old_t) || !is_eqp(std::get<1>(r), old_v) || !is_eqp(std::get<2>(r), old_b))
-        return mk_let(let_name(e), std::get<0>(r), std::get<1>(r), std::get<2>(r));
-    else
-        return e;
-}
-template<typename F> expr update_metavar(expr const & e, name const & n, F f) {
-    static_assert(std::is_same<typename std::result_of<F(local_entry const &)>::type, local_entry>::value,
-                  "update_metavar: return type of f(local_entry) is not local_entry");
-    buffer<local_entry> new_entries;
-    bool modified = n != metavar_name(e);
-    for (local_entry const & me : metavar_lctx(e)) {
-        local_entry new_me = f(me);
-        if (new_me.kind() != me.kind() || new_me.s() != me.s()) {
-            modified = true;
-        } else if (new_me.is_inst()) {
-            if (!is_eqp(new_me.v(), me.v()))
-                modified = true;
-        } else if (new_me.n() != me.n()) {
-            modified = true;
-        }
-        new_entries.push_back(new_me);
-    }
-    if (modified)
-        return mk_metavar(n, to_list(new_entries.begin(), new_entries.end()));
-    else
-        return e;
-}
-template<typename F> expr update_metavar(expr const & e, F f) {
-    static_assert(std::is_same<typename std::result_of<F(local_entry const &)>::type, local_entry>::value,
-                  "update_metavar: return type of f(local_entry) is not local_entry");
-    return update_metavar(e, metavar_name(e), f);
-}
-inline expr update_metavar(expr const & e, local_context const & lctx) {
-    if (metavar_lctx(e) != lctx)
-        return mk_metavar(metavar_name(e), lctx);
-    else
-        return e;
-}
-inline expr update_const(expr const & e, optional<expr> const & t) {
-    if (!is_eqp(const_type(e), t))
-        return mk_constant(const_name(e), t);
-    else
-        return e;
-}
-template<typename F> expr update_pair(expr const & e, F f) {
-    expr const & old_f  = pair_first(e);
-    expr const & old_s  = pair_second(e);
-    expr const & old_t  = pair_type(e);
-    auto r = f(old_f, old_s, old_t);
-    if (!is_eqp(std::get<0>(r), old_t) || !is_eqp(std::get<1>(r), old_s) || !is_eqp(std::get<2>(r), old_t))
-        return mk_pair(std::get<0>(r), std::get<1>(r), std::get<2>(r));
-    else
-        return e;
-}
-inline expr update_pair(expr const & e, expr const & new_f, expr const & new_s, expr const & new_t) {
-    return update_pair(e, [&](expr const &, expr const &, expr const &) { return std::make_tuple(new_f, new_s, new_t); });
-}
-inline expr update_proj(expr const & e, expr const & new_arg) {
-    if (!is_eqp(proj_arg(e), new_arg))
-        return mk_proj(proj_first(e), new_arg);
-    else
-        return e;
-}
-inline expr update_heq(expr const & e, expr const & new_lhs, expr const & new_rhs) {
-    if (!is_eqp(heq_lhs(e), new_lhs) || !is_eqp(heq_rhs(e), new_rhs))
-        return mk_heq(new_lhs, new_rhs);
-    else
-        return e;
-}
+expr update_app(expr const & e, expr const & new_fn, expr const & new_arg);
+expr update_proj(expr const & e, expr const & new_arg);
+expr update_pair(expr const & e, expr const & new_first, expr const & new_second, expr const & new_type);
+expr update_binder(expr const & e, expr const & new_domain, expr const & new_body);
+expr update_let(expr const & e, optional<expr> const & new_type, expr const & new_val, expr const & new_body);
+expr update_mlocal(expr const & e, expr const & new_type);
 // =======================================
 
-
 // =======================================
 // Serializer/Deserializer
 serializer & operator<<(serializer & s, expr const & e);
@@ -714,5 +575,4 @@ inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d);
 // =======================================
 
 std::ostream & operator<<(std::ostream & out, expr const & e);
-#endif
 }
diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h
deleted file mode 100644
index 28fa25154..000000000
--- a/src/kernel/expr_eq.h
+++ /dev/null
@@ -1,102 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <memory>
-#include "util/interrupt.h"
-#include "kernel/expr.h"
-#include "kernel/expr_sets.h"
-
-namespace lean {
-/** \brief Identity function for expressions. */
-struct id_expr_fn {
-    expr const & operator()(expr const & e) const { return e; }
-};
-
-/**
-   \brief Functional object for comparing expressions.
-   The parameter N is a normalization function that can be used
-   to normalize sub-expressions before comparing them.
-   The hashcode of expressions is used to optimize the comparison when
-   parameter UseHash == true. We should set UseHash to false when N
-   is not the identity function.
-*/
-template<typename N = id_expr_fn, bool UseHash = true>
-class expr_eq_fn {
-    std::unique_ptr<expr_cell_pair_set> m_eq_visited;
-    N                                   m_norm;
-
-    bool apply(optional<expr> const & a0, optional<expr> const & b0) {
-        if (is_eqp(a0, b0))
-            return true;
-        else if (!a0 || !b0)
-            return false;
-        else
-            return apply(*a0, *b0);
-    }
-
-    bool apply(expr const & a0, expr const & b0) {
-        check_system("expression equality test");
-        if (is_eqp(a0, b0))                    return true;
-        if (UseHash && a0.hash() != b0.hash()) return false;
-        expr const & a = m_norm(a0);
-        expr const & b = m_norm(b0);
-        if (a.kind() != b.kind())            return false;
-        if (is_var(a))                       return var_idx(a) == var_idx(b);
-        if (is_shared(a) && is_shared(b)) {
-            auto p = std::make_pair(a.raw(), b.raw());
-            if (!m_eq_visited)
-                m_eq_visited.reset(new expr_cell_pair_set);
-            if (m_eq_visited->find(p) != m_eq_visited->end())
-                return true;
-            m_eq_visited->insert(p);
-        }
-        switch (a.kind()) {
-        case expr_kind::Var:      lean_unreachable(); // LCOV_EXCL_LINE
-        case expr_kind::Constant: return const_name(a) == const_name(b);
-        case expr_kind::App:
-            if (num_args(a) != num_args(b))
-                return false;
-            for (unsigned i = 0; i < num_args(a); i++)
-                if (!apply(arg(a, i), arg(b, i)))
-                    return false;
-            return true;
-        case expr_kind::HEq:      return heq_lhs(a) == heq_lhs(b) && heq_rhs(a) == heq_rhs(b);
-        case expr_kind::Pair:     return pair_first(a) == pair_first(b) && pair_second(a) == pair_second(b) && pair_type(a) == pair_type(b);
-        case expr_kind::Proj:     return proj_first(a) == proj_first(b) && proj_arg(a) == proj_arg(b);
-        case expr_kind::Sigma:
-        case expr_kind::Lambda:   // Remark: we ignore get_abs_name because we want alpha-equivalence
-        case expr_kind::Pi:       return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b));
-        case expr_kind::Type:     return ty_level(a) == ty_level(b);
-        case expr_kind::Value:    return to_value(a) == to_value(b);
-        case expr_kind::Let:      return apply(let_type(a), let_type(b)) && apply(let_value(a), let_value(b)) && apply(let_body(a), let_body(b));
-        case expr_kind::MetaVar:
-            return
-                metavar_name(a) == metavar_name(b) &&
-                compare(metavar_lctx(a), metavar_lctx(b), [&](local_entry const & e1, local_entry const & e2) {
-                        if (e1.kind() != e2.kind() || e1.s() != e2.s())
-                            return false;
-                        if (e1.is_inst())
-                            return apply(e1.v(), e2.v());
-                        else
-                            return e1.n() == e2.n();
-                    });
-        }
-        lean_unreachable(); // LCOV_EXCL_LINE
-    }
-public:
-    expr_eq_fn(N const & norm = N()):m_norm(norm) {
-        // the return type of N()(e) should be expr const &
-        static_assert(std::is_same<typename std::result_of<decltype(std::declval<N>())(expr const &)>::type,
-                      expr const &>::value,
-                      "The return type of CMP()(k1, k2) is not int.");
-    }
-    bool operator()(expr const & a, expr const & b) {
-        return apply(a, b);
-    }
-    void clear() { m_eq_visited.reset(); }
-};
-}
diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
new file mode 100644
index 000000000..153bd237e
--- /dev/null
+++ b/src/kernel/expr_eq_fn.cpp
@@ -0,0 +1,71 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/expr_eq_fn.h"
+
+namespace lean {
+bool expr_eq_fn::apply(optional<expr> const & a0, optional<expr> const & b0) {
+    if (is_eqp(a0, b0))
+        return true;
+    else if (!a0 || !b0)
+        return false;
+    else
+        return apply(*a0, *b0);
+}
+
+bool expr_eq_fn::apply(expr const & a, expr const & b) {
+    check_system("expression equality test");
+    if (is_eqp(a, b))          return true;
+    if (a.hash() != b.hash())  return false;
+    if (a.kind() != b.kind())  return false;
+    if (is_var(a))             return var_idx(a) == var_idx(b);
+    if (is_shared(a) && is_shared(b)) {
+        auto p = std::make_pair(a.raw(), b.raw());
+        if (!m_eq_visited)
+            m_eq_visited.reset(new expr_cell_pair_set);
+        if (m_eq_visited->find(p) != m_eq_visited->end())
+            return true;
+        m_eq_visited->insert(p);
+    }
+    switch (a.kind()) {
+    case expr_kind::Var:
+        lean_unreachable(); // LCOV_EXCL_LINE
+    case expr_kind::Constant:
+        return
+            const_name(a) == const_name(b) &&
+            compare(const_level_params(a), const_level_params(b), [](level const & l1, level const & l2) { return l1 == l2; });
+    case expr_kind::Local: case expr_kind::Meta:
+        return
+            mlocal_name(a) == mlocal_name(b) &&
+            apply(mlocal_type(a), mlocal_type(b));
+    case expr_kind::App:
+        return
+            apply(app_fn(a), app_fn(b)) &&
+            apply(app_arg(a), app_arg(b));
+    case expr_kind::Pair:
+        return
+            apply(pair_first(a), pair_first(b)) &&
+            apply(pair_second(a), pair_second(b)) &&
+            apply(pair_type(a), pair_type(b));
+    case expr_kind::Fst: case expr_kind::Snd:
+        return apply(proj_arg(a), proj_arg(b));
+    case expr_kind::Sigma: case expr_kind::Lambda: case expr_kind::Pi:
+        return
+            apply(binder_domain(a), binder_domain(b)) &&
+            apply(binder_body(a), binder_body(b));
+    case expr_kind::Sort:
+        return sort_level(a) == sort_level(b);
+    case expr_kind::Macro:
+        return to_macro(a) == to_macro(b);
+    case expr_kind::Let:
+        return
+            apply(let_type(a), let_type(b)) &&
+            apply(let_value(a), let_value(b)) &&
+            apply(let_body(a), let_body(b));
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
+}
diff --git a/src/kernel/expr_eq_fn.h b/src/kernel/expr_eq_fn.h
new file mode 100644
index 000000000..b96014495
--- /dev/null
+++ b/src/kernel/expr_eq_fn.h
@@ -0,0 +1,25 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <memory>
+#include "util/interrupt.h"
+#include "kernel/expr.h"
+#include "kernel/expr_sets.h"
+
+namespace lean {
+/**
+   \brief Functional object for comparing expressions.
+*/
+class expr_eq_fn {
+    std::unique_ptr<expr_cell_pair_set> m_eq_visited;
+    bool apply(optional<expr> const & a0, optional<expr> const & b0);
+    bool apply(expr const & a, expr const & b);
+public:
+    bool operator()(expr const & a, expr const & b) { return apply(a, b); }
+    void clear() { m_eq_visited.reset(); }
+};
+}