diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 46331d21a..541946dc4 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp
-  instantiate.cpp deep_copy.cpp normalize.cpp)
+  instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp)
 target_link_libraries(kernel ${EXTRA_LIBS})
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
new file mode 100644
index 000000000..34a82b9e6
--- /dev/null
+++ b/src/kernel/environment.cpp
@@ -0,0 +1,160 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <algorithm>
+#include <vector>
+#include <limits>
+#include "environment.h"
+#include "exception.h"
+#include "debug.h"
+
+namespace lean {
+constexpr unsigned uninit = std::numeric_limits<int>::max();
+
+struct environment::imp {
+    std::vector<std::vector<unsigned>> m_uvar_distances;
+    std::vector<level>                 m_uvars;
+
+    static int sub(int v, unsigned k) {
+        long long r = static_cast<long long>(v) - static_cast<long long>(k);
+        if (r < std::numeric_limits<int>::min())
+            throw exception("universe overflow");
+        return static_cast<int>(r);
+    }
+
+    static int add(int v, unsigned k) {
+        long long r = static_cast<long long>(v) + static_cast<long long>(k);
+        if (r > std::numeric_limits<int>::max() - 1)
+            throw exception("universe overflow");
+        return static_cast<int>(r);
+    }
+
+    static unsigned add(unsigned v, unsigned k) {
+        unsigned long long r = static_cast<unsigned long long>(v) + static_cast<unsigned long long>(k);
+        if (r > std::numeric_limits<int>::max() - 1)
+            throw exception("universe overflow");
+        return static_cast<unsigned>(r);
+    }
+
+    /** \brief Return true iff l1 >= l2 + k */
+    bool is_implied(level const & l1, level const & l2, int k) {
+        switch (kind(l2)) {
+        case level_kind::UVar:
+            switch (kind(l1)) {
+            case level_kind::UVar: {
+                unsigned d = m_uvar_distances[uvar_idx(l1)][uvar_idx(l2)];
+                return k >= 0 && d != uninit && d >= static_cast<unsigned>(k);
+            }
+            case level_kind::Lift: return is_implied(lift_of(l1), l2, sub(k, lift_offset(l1)));
+            case level_kind::Max:  return is_implied(max_level1(l1), l2, k) || is_implied(max_level2(l1), l2, k);
+            }
+        case level_kind::Lift: return is_implied(l1, lift_of(l2), add(k, lift_offset(l2)));
+        case level_kind::Max:  return is_implied(l1, max_level1(l2), k) && is_implied(l1, max_level2(l2), k);
+        }
+        lean_unreachable();
+        return false;
+    }
+
+    bool is_implied(level const & l1, level const & l2) {
+        return is_implied(l1, l2, 0);
+    }
+
+    level add_var(name const & n) {
+        if (std::any_of(m_uvars.begin(), m_uvars.end(), [&](level const & l){ return uvar_name(l) == n; }))
+            throw exception("invalid universe variable declaration, it has already been declared");
+        unsigned idx = m_uvars.size();
+        level r(n, idx);
+        m_uvars.push_back(r);
+        std::for_each(m_uvar_distances.begin(), m_uvar_distances.end(), [](std::vector<unsigned> & v) { v.push_back(uninit); });
+        m_uvar_distances.push_back(std::vector<unsigned>());
+        std::vector<unsigned> & d = m_uvar_distances.back();
+        d.resize(m_uvars.size(), static_cast<unsigned>(uninit));
+        d[idx] = 0;
+        return r;
+    }
+
+    void add_constraint(uvar v1, uvar v2, unsigned d) {
+        lean_assert(v1 != v2);
+        unsigned num = m_uvar_distances.size();
+        lean_assert(v1 < num);
+        lean_assert(v2 < num);
+        std::vector<unsigned> & v1_dists = m_uvar_distances[v1];
+        v1_dists[v2] = d;
+        // update forward
+        std::vector<unsigned> & v2_dists = m_uvar_distances[v2];
+        for (uvar v3 = 0; v3 < num; v3++) {
+            if (v2_dists[v3] != uninit) {
+                lean_assert(v1 != v3);
+                unsigned d_v1_v3 = add(d, v2_dists[v3]);
+                if (v1_dists[v3] == uninit || d_v1_v3 >= v1_dists[v3])
+                    v1_dists[v3] = d_v1_v3;
+            }
+        }
+    }
+
+    void add_constraints(uvar v1, level const & l, unsigned k) {
+        switch (kind(l)) {
+        case level_kind::UVar: add_constraint(v1, uvar_idx(l), k);                   return;
+        case level_kind::Lift: add_constraints(v1, lift_of(l), add(k, lift_offset(l)));  return;
+        case level_kind::Max:  add_constraints(v1, max_level1(l), k); add_constraints(v1, max_level2(l), k); return;
+        }
+        lean_unreachable();
+    }
+
+    level define_uvar(name const & n, level const & l) {
+        level r = add_var(n);
+        add_constraints(uvar_idx(r), l, 0);
+        return r;
+    }
+
+    void init_uvars() {
+        m_uvars.push_back(level());
+        m_uvar_distances.push_back(std::vector<unsigned>());
+        m_uvar_distances.back().push_back(0);
+        lean_assert(uvar_idx(m_uvars.back()) == 0);
+    }
+
+    void display_uvars(std::ostream & out) const {
+        std::for_each(m_uvars.begin(), m_uvars.end(),
+                      [&](level const & u) {
+                          std::vector<unsigned> const & u_dists = m_uvar_distances[uvar_idx(u)];
+                          unsigned num = u_dists.size();
+                          for (uvar v2 = 0; v2 < num; v2++) {
+                              if (v2 != uvar_idx(u) && u_dists[v2] != uninit) {
+                                  out << uvar_name(u) << "  >= " << uvar_name(m_uvars[v2]);
+                                  if (u_dists[v2] > 0)
+                                      out << " + " << u_dists[v2];
+                                  out << "\n";
+                              }
+                          }
+                          out << "\n";
+                      });
+    }
+
+    imp() {
+        init_uvars();
+    }
+};
+
+environment::environment():
+    m_imp(new imp) {
+}
+
+environment::~environment() {
+}
+
+level environment::define_uvar(name const & n, level const & l) {
+    return m_imp->define_uvar(n, l);
+}
+
+bool environment::is_implied(level const & l1, level const & l2) const {
+    return m_imp->is_implied(l1, l2);
+}
+
+void environment::display_uvars(std::ostream & out) const {
+    m_imp->display_uvars(out);
+}
+}
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
new file mode 100644
index 000000000..0bf80237d
--- /dev/null
+++ b/src/kernel/environment.h
@@ -0,0 +1,43 @@
+/*
+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 <iostream>
+#include <memory>
+#include "level.h"
+
+namespace lean {
+/**
+   \brief Lean environment for defining constants, inductive
+   datatypes, universe variables, et.c
+*/
+class environment {
+    struct imp;
+    std::unique_ptr<imp> m_imp;
+public:
+    environment();
+    ~environment();
+
+    /**
+       \brief Define a new universe variable with name \c n and constraint <tt>n >= l</tt>.
+       Return the new variable.
+
+       \remark An exception is thrown if a universe inconsistency is detected.
+    */
+    level define_uvar(name const & n, level const & l);
+    level define_uvar(name const & n) { return define_uvar(n, level()); }
+    level define_uvar(char const * n, level const & l) { return define_uvar(name(n), l); }
+    level define_uvar(char const * n) { return define_uvar(name(n), level()); }
+
+    /**
+       \brief Return true iff the constraint l1 >= l2 is implied by the constraints
+       in the environment.
+    */
+    bool is_implied(level const & l1, level const & l2) const;
+
+    void display_uvars(std::ostream & out) const;
+};
+}
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
new file mode 100644
index 000000000..7da11942f
--- /dev/null
+++ b/src/kernel/level.cpp
@@ -0,0 +1,88 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "level.h"
+#include "rc.h"
+#include "debug.h"
+
+namespace lean {
+struct level_cell {
+    void dealloc();
+    MK_LEAN_RC()
+    level_kind m_kind;
+    level_cell(level_kind k):m_rc(1), m_kind(k) {}
+};
+struct level_uvar : public level_cell {
+    name m_name;
+    uvar m_uvar;
+    level_uvar(name const & n, uvar u):level_cell(level_kind::UVar), m_name(n), m_uvar(u) {}
+};
+struct level_lift : public level_cell {
+    level    m_l;
+    unsigned m_k;
+    level_lift(level const & l, unsigned k):level_cell(level_kind::Lift), m_l(l), m_k(k) {}
+};
+struct level_max : public level_cell {
+    level m_l1;
+    level m_l2;
+    level_max(level const & l1, level const & l2):level_cell(level_kind::Max), m_l1(l1), m_l2(l2) {}
+};
+void level_cell::dealloc() {
+    switch (m_kind) {
+    case level_kind::UVar:    delete static_cast<level_uvar*>(this); break;
+    case level_kind::Lift:    delete static_cast<level_lift*>(this); break;
+    case level_kind::Max:     delete static_cast<level_max*> (this); break;
+    }
+}
+level::level():                                  m_ptr(new level_uvar(name("bot"), 0)) { lean_assert(uvar_name(*this) == name("bot")); }
+level::level(name const & n, uvar u):            m_ptr(new level_uvar(n, u)) {}
+level::level(level const & l, unsigned k):       m_ptr(new level_lift(l, k)) {}
+level::level(level const & l1, level const & l2):m_ptr(new level_max(l1, l2)) {}
+level::level(level const & s):
+    m_ptr(s.m_ptr) {
+    if (m_ptr)
+        m_ptr->inc_ref();
+}
+level::level(level && s):
+    m_ptr(s.m_ptr) {
+    s.m_ptr = 0;
+}
+level::~level() {
+    if (m_ptr)
+        m_ptr->dec_ref();
+}
+
+level_kind    kind       (level const & l) { lean_assert(l.m_ptr); return l.m_ptr->m_kind; }
+name const &  uvar_name  (level const & l) { lean_assert(is_uvar(l)); return static_cast<level_uvar*>(l.m_ptr)->m_name; }
+uvar          uvar_idx   (level const & l) { lean_assert(is_uvar(l)); return static_cast<level_uvar*>(l.m_ptr)->m_uvar; }
+level const & lift_of    (level const & l) { lean_assert(is_lift(l)); return static_cast<level_lift*>(l.m_ptr)->m_l; }
+unsigned      lift_offset(level const & l) { lean_assert(is_lift(l)); return static_cast<level_lift*>(l.m_ptr)->m_k; }
+level const & max_level1 (level const & l) { lean_assert(is_max(l));  return static_cast<level_max*>(l.m_ptr)->m_l1; }
+level const & max_level2 (level const & l) { lean_assert(is_max(l));  return static_cast<level_max*>(l.m_ptr)->m_l2; }
+
+level & level::operator=(level const & l) { LEAN_COPY_REF(level, l); }
+level & level::operator=(level&& l) { LEAN_MOVE_REF(level, l); }
+
+bool operator==(level const & l1, level const & l2) {
+    if (kind(l1) != kind(l2)) return false;
+    switch (kind(l1)) {
+    case level_kind::UVar: return uvar_idx(l1)   == uvar_idx(l2);
+    case level_kind::Lift: return lift_of(l1)    == lift_of(l2)    && lift_offset(l1) == lift_offset(l2);
+    case level_kind::Max:  return max_level1(l1) == max_level1(l2) && max_level2(l1)  == max_level2(l2);
+    }
+    lean_unreachable();
+    return false;
+}
+
+std::ostream & operator<<(std::ostream & out, level const & l) {
+    switch (kind(l)) {
+    case level_kind::UVar: out << uvar_name(l);                                            return out;
+    case level_kind::Lift: out << lift_of(l) << " + " << lift_offset(l);                   return out;
+    case level_kind::Max:  out << "max(" << max_level1(l) << ", " << max_level2(l) << ")"; return out;
+    }
+    return out;
+}
+}
diff --git a/src/kernel/level.h b/src/kernel/level.h
new file mode 100644
index 000000000..149cdba6c
--- /dev/null
+++ b/src/kernel/level.h
@@ -0,0 +1,53 @@
+/*
+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 <iostream>
+#include "name.h"
+
+namespace lean {
+class environment;
+struct level_cell;
+typedef unsigned uvar;
+enum class level_kind { UVar, Lift, Max };
+/**
+   \brief Universe level.
+*/
+class level {
+    friend class environment;
+    level_cell * m_ptr;
+    level(name const & n, uvar u);
+public:
+    level();
+    level(level const & l, unsigned k);
+    level(level const & l1, level const & l2);
+    level(level const & l);
+    level(level&& s);
+    ~level();
+
+    friend level_kind    kind       (level const & l);
+    friend name const &  uvar_name  (level const & l);
+    friend uvar          uvar_idx   (level const & l);
+    friend level const & lift_of    (level const & l);
+    friend unsigned      lift_offset(level const & l);
+    friend level const & max_level1 (level const & l);
+    friend level const & max_level2 (level const & l);
+
+    level & operator=(level const & l);
+    level & operator=(level&& l);
+
+    friend bool operator==(level const & l1, level const & l2);
+    friend bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); }
+    friend void swap(level & l1, level & l2) { std::swap(l1, l2); }
+
+    friend std::ostream & operator<<(std::ostream & out, level const & l);
+};
+inline level max(level const & l1, level const & l2) { return level(l1, l2); }
+inline level operator+(level const & l, unsigned k)  { return level(l, k); }
+inline bool is_uvar(level const & l) { return kind(l) == level_kind::UVar;  }
+inline bool is_lift(level const & l) { return kind(l) == level_kind::Lift; }
+inline bool is_max (level const & l) { return kind(l) == level_kind::Max;  }
+}
diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt
index f9f637f3e..8f3a1dcc5 100644
--- a/src/tests/kernel/CMakeLists.txt
+++ b/src/tests/kernel/CMakeLists.txt
@@ -10,3 +10,6 @@ add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads)
 add_executable(free_vars free_vars.cpp)
 target_link_libraries(free_vars ${EXTRA_LIBS})
 add_test(free_vars ${CMAKE_CURRENT_BINARY_DIR}/free_vars)
+add_executable(level level.cpp)
+target_link_libraries(level ${EXTRA_LIBS})
+add_test(level ${CMAKE_CURRENT_BINARY_DIR}/level)
diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp
new file mode 100644
index 000000000..4a4d0701e
--- /dev/null
+++ b/src/tests/kernel/level.cpp
@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <locale>
+#include "environment.h"
+#include "test.h"
+using namespace lean;
+
+static void tst1() {
+    environment env;
+    level l1 = env.define_uvar("l1", level());
+    level l2 = env.define_uvar("l2", l1 + 10);
+    level l3 = env.define_uvar("l3", max(l2, l1 + 3));
+    level l4 = env.define_uvar("l4", max(l1 + 8, max(l2 + 2, l3 + 20)));
+    env.display_uvars(std::cout);
+    lean_assert(env.is_implied(l4 + 10, l3 + 30));
+    lean_assert(!env.is_implied(l4 + 9, l3 + 30));
+}
+
+int main() {
+    continue_on_violation(true);
+    tst1();
+    return has_violations() ? 1 : 0;
+}
diff --git a/src/util/list.h b/src/util/list.h
index 884d3387c..9f4ae643e 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -33,22 +33,8 @@ public:
     list(list&& s):m_ptr(s.m_ptr) { s.m_ptr = 0; }
     ~list() { if (m_ptr) m_ptr->dec_ref(); }
 
-    list & operator=(list const & s) {
-        if (s.m_ptr)
-            s.m_ptr->inc_ref();
-        if (m_ptr)
-            m_ptr->dec_ref();
-        m_ptr = s.m_ptr;
-        return *this;
-    }
-
-    list & operator=(list && s) {
-        if (m_ptr)
-            m_ptr->dec_ref();
-        m_ptr   = s.m_ptr;
-        s.m_ptr = 0;
-        return *this;
-    }
+    list & operator=(list const & s) { LEAN_COPY_REF(list, s); }
+    list & operator=(list && s) { LEAN_MOVE_REF(list, s); }
 
     friend bool is_nil(list const & l) { return l.m_ptr == nullptr; }
     friend T const & head(list const & l) { lean_assert(!is_nil(l)); return l.m_ptr->m_head; }
diff --git a/src/util/name.cpp b/src/util/name.cpp
index d8480a1f4..7dbd7fbfd 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -77,35 +77,35 @@ struct name::imp {
 };
 
 name::name(imp * p) {
-    m_imp = p;
-    if (m_imp)
-        m_imp->inc_ref();
+    m_ptr = p;
+    if (m_ptr)
+        m_ptr->inc_ref();
 }
 
 name::name() {
-    m_imp = nullptr;
+    m_ptr = nullptr;
 }
 
 name::name(name const & prefix, char const * name) {
     size_t sz  = strlen(name);
     lean_assert(sz < 1u<<31);
     char * mem = new char[sizeof(imp) + sz + 1];
-    m_imp      = new (mem) imp(true, prefix.m_imp);
+    m_ptr      = new (mem) imp(true, prefix.m_ptr);
     std::memcpy(mem + sizeof(imp), name, sz + 1);
-    m_imp->m_str       = mem + sizeof(imp);
-    if (m_imp->m_prefix)
-        m_imp->m_hash = hash_str(sz, name, m_imp->m_prefix->m_hash);
+    m_ptr->m_str       = mem + sizeof(imp);
+    if (m_ptr->m_prefix)
+        m_ptr->m_hash = hash_str(sz, name, m_ptr->m_prefix->m_hash);
     else
-        m_imp->m_hash = hash_str(sz, name, 0);
+        m_ptr->m_hash = hash_str(sz, name, 0);
 }
 
 name::name(name const & prefix, unsigned k) {
-    m_imp      = new imp(false, prefix.m_imp);
-    m_imp->m_k = k;
-    if (m_imp->m_prefix)
-        m_imp->m_hash = ::lean::hash(m_imp->m_prefix->m_hash, k);
+    m_ptr      = new imp(false, prefix.m_ptr);
+    m_ptr->m_k = k;
+    if (m_ptr->m_prefix)
+        m_ptr->m_hash = ::lean::hash(m_ptr->m_prefix->m_hash, k);
     else
-        m_imp->m_hash = k;
+        m_ptr->m_hash = k;
 }
 
 name::name(char const * n):name(name(), n) {
@@ -114,57 +114,43 @@ name::name(char const * n):name(name(), n) {
 name::name(unsigned k):name(name(), k) {
 }
 
-name::name(name const & other):m_imp(other.m_imp) {
-    m_imp->inc_ref();
+name::name(name const & other):m_ptr(other.m_ptr) {
+    m_ptr->inc_ref();
 }
 
-name::name(name && other):m_imp(other.m_imp) {
-    other.m_imp = 0;
+name::name(name && other):m_ptr(other.m_ptr) {
+    other.m_ptr = 0;
 }
 
 name::~name() {
-    if (m_imp)
-        m_imp->dec_ref();
+    if (m_ptr)
+        m_ptr->dec_ref();
 }
 
-name & name::operator=(name const & other) {
-    if (other.m_imp)
-        other.m_imp->inc_ref();
-    if (m_imp)
-        m_imp->dec_ref();
-    m_imp = other.m_imp;
-    return *this;
-}
+name & name::operator=(name const & other) { LEAN_COPY_REF(name, other); }
 
-name & name::operator=(name && other) {
-    lean_assert(this != &other);
-    if (m_imp)
-        m_imp->dec_ref();
-    m_imp       = other.m_imp;
-    other.m_imp = 0;
-    return *this;
-}
+name & name::operator=(name && other) { LEAN_MOVE_REF(name, other); }
 
 name_kind name::kind() const {
-    if (m_imp == nullptr)
+    if (m_ptr == nullptr)
         return name_kind::ANONYMOUS;
     else
-        return m_imp->m_is_string ? name_kind::STRING : name_kind::NUMERAL;
+        return m_ptr->m_is_string ? name_kind::STRING : name_kind::NUMERAL;
 }
 
 unsigned name::get_numeral() const {
     lean_assert(is_numeral());
-    return m_imp->m_k;
+    return m_ptr->m_k;
 }
 
 char const * name::get_string() const {
     lean_assert(is_string());
-    return m_imp->m_str;
+    return m_ptr->m_str;
 }
 
 bool operator==(name const & a, name const & b) {
-    name::imp * i1 = a.m_imp;
-    name::imp * i2 = b.m_imp;
+    name::imp * i1 = a.m_ptr;
+    name::imp * i2 = b.m_ptr;
     while (true) {
         if (i1 == i2)
             return true;
@@ -218,12 +204,12 @@ int cmp(name::imp * i1, name::imp * i2) {
 }
 
 bool name::is_atomic() const {
-    return m_imp == nullptr || m_imp->m_prefix == nullptr;
+    return m_ptr == nullptr || m_ptr->m_prefix == nullptr;
 }
 
 name name::get_prefix() const {
     lean_assert(!is_atomic());
-    return name(m_imp->m_prefix);
+    return name(m_ptr->m_prefix);
 }
 
 static unsigned num_digits(unsigned k) {
@@ -238,11 +224,11 @@ static unsigned num_digits(unsigned k) {
 }
 
 size_t name::size(char const * sep) const {
-    if (m_imp == nullptr) {
+    if (m_ptr == nullptr) {
         return strlen(anonymous_str);
     }
     else {
-        imp * i       = m_imp;
+        imp * i       = m_ptr;
         size_t sep_sz = strlen(sep);
         size_t r      = 0;
         while (true) {
@@ -265,18 +251,18 @@ size_t name::size(char const * sep) const {
 }
 
 unsigned name::hash() const {
-    return m_imp->m_hash;
+    return m_ptr->m_hash;
 }
 
 std::ostream & operator<<(std::ostream & out, name const & n) {
-    name::imp::display(out, default_name_separator, n.m_imp);
+    name::imp::display(out, default_name_separator, n.m_ptr);
     return out;
 }
 
 name::sep::sep(name const & n, char const * s):m_name(n), m_sep(s) {}
 
 std::ostream & operator<<(std::ostream & out, name::sep const & s) {
-    name::imp::display(out, s.m_sep, s.m_name.m_imp);
+    name::imp::display(out, s.m_sep, s.m_name.m_ptr);
     return out;
 }
 
diff --git a/src/util/name.h b/src/util/name.h
index 9b00f0de7..62abcc3a4 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -18,7 +18,7 @@ enum class name_kind { ANONYMOUS, STRING, NUMERAL };
 class name {
     struct imp;
     friend int cmp(imp * i1, imp * i2);
-    imp * m_imp;
+    imp * m_ptr;
     explicit name(imp * p);
 public:
     name();
@@ -34,7 +34,7 @@ public:
     friend bool operator==(name const & a, name const & b);
     friend bool operator!=(name const & a, name const & b) { return !(a == b); }
     // total order on hierarchical names.
-    friend int cmp(name const & a, name const & b) { return cmp(a.m_imp, b.m_imp); }
+    friend int cmp(name const & a, name const & b) { return cmp(a.m_ptr, b.m_ptr); }
     friend bool operator<(name const & a, name const & b) { return cmp(a, b) < 0; }
     friend bool operator>(name const & a, name const & b) { return cmp(a, b) > 0; }
     friend bool operator<=(name const & a, name const & b) { return cmp(a, b) <= 0; }
diff --git a/src/util/rc.h b/src/util/rc.h
index 1ffdc59df..176e30935 100644
--- a/src/util/rc.h
+++ b/src/util/rc.h
@@ -30,3 +30,18 @@ void inc_ref() { std::atomic_fetch_add_explicit(&m_rc, 1u, std::memory_order_rel
 bool dec_ref_core() { lean_assert(get_rc() > 0); return std::atomic_fetch_sub_explicit(&m_rc, 1u, std::memory_order_relaxed) == 1u; } \
 void dec_ref() { if (dec_ref_core()) dealloc(); }
 #endif
+
+#define LEAN_COPY_REF(T, Arg)                   \
+    if (Arg.m_ptr)                              \
+        Arg.m_ptr->inc_ref();                   \
+    if (m_ptr)                                  \
+        m_ptr->dec_ref();                       \
+    m_ptr = Arg.m_ptr;                          \
+    return *this;
+
+#define LEAN_MOVE_REF(T, Arg)                   \
+    if (m_ptr)                                  \
+        m_ptr->dec_ref();                       \
+    m_ptr   = Arg.m_ptr;                        \
+    Arg.m_ptr = 0;                              \
+    return *this;
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp
index 5f9ca09e7..cf3b3c68d 100644
--- a/src/util/sexpr/sexpr.cpp
+++ b/src/util/sexpr/sexpr.cpp
@@ -129,22 +129,8 @@ mpq const & sexpr::get_mpq() const { return static_cast<sexpr_mpq*>(m_ptr)->m_va
 
 unsigned sexpr::hash() const { return m_ptr == nullptr ? 23 : m_ptr->m_hash; }
 
-sexpr & sexpr::operator=(sexpr const & s) {
-    if (s.m_ptr)
-        s.m_ptr->inc_ref();
-    if (m_ptr)
-        m_ptr->dec_ref();
-    m_ptr = s.m_ptr;
-    return *this;
-}
-
-sexpr & sexpr::operator=(sexpr && s) {
-    if (m_ptr)
-        m_ptr->dec_ref();
-    m_ptr   = s.m_ptr;
-    s.m_ptr = 0;
-    return *this;
-}
+sexpr & sexpr::operator=(sexpr const & s) { LEAN_COPY_REF(sexpr, s); }
+sexpr & sexpr::operator=(sexpr && s) { LEAN_MOVE_REF(sexpr, s); }
 
 bool is_list(sexpr const & s) {
     if (is_nil(s))