diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index da1ee20bb..28704ed56 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -7,9 +7,10 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include <limits>
-#include "name.h"
 #include "rc.h"
+#include "name.h"
 #include "mpz.h"
+#include "hash.h"
 
 namespace lean {
 /* =======================================
@@ -309,12 +310,22 @@ inline mpz const &  get_numeral(expr const & e)              { return to_numeral
 inline bool operator!=(expr const & a, expr const & b) { return !operator==(a, b); }
 // =======================================
 
+// =======================================
+// Expression+Offset
+typedef std::pair<expr, unsigned>       expr_offset;
+typedef std::pair<expr_cell*, unsigned> expr_cell_offset;
+// =======================================
+
 // =======================================
 // Auxiliary functors
 struct expr_hash { unsigned operator()(expr const & e) const { return e.hash(); } };
 struct expr_eqp { bool operator()(expr const & e1, expr const & e2) const { return eqp(e1, e2); } };
 struct expr_cell_hash { unsigned operator()(expr_cell * e) const { return e->hash(); } };
 struct expr_cell_eqp { bool operator()(expr_cell * e1, expr_cell * e2) const { return e1 == e2; } };
+struct expr_offset_hash { unsigned operator()(expr_offset const & p) const { return hash(p.first.hash(), p.second); } };
+struct expr_offset_eqp { unsigned operator()(expr_offset const & p1, expr_offset const & p2) const { return eqp(p1.first, p2.first) && p1.second == p2.second; } };
+struct expr_cell_offset_hash { unsigned operator()(expr_cell_offset const & p) const { return hash(p.first->hash(), p.second); } };
+struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, expr_cell_offset const & p2) const { return p1 == p2; } };
 // =======================================
 
 // =======================================
diff --git a/src/kernel/sets.h b/src/kernel/sets.h
index 6218530c8..5e78f9e0b 100644
--- a/src/kernel/sets.h
+++ b/src/kernel/sets.h
@@ -12,9 +12,10 @@ Author: Leonardo de Moura
 namespace lean {
 
 // =======================================
-// Expression Set
+// Expression Set && Expression Offset Set
 // Remark: to expressions are assumed to be equal if they are "pointer-equal"
 typedef std::unordered_set<expr, expr_hash, expr_eqp> expr_set;
+typedef std::unordered_set<expr_offset, expr_offset_hash, expr_offset_eqp> expr_offset_set;
 // =======================================
 
 // =======================================
@@ -25,6 +26,7 @@ typedef std::unordered_set<expr, expr_hash, expr_eqp> expr_set;
 // does not prevent an expression from being
 // garbage collected.
 typedef std::unordered_set<expr_cell*, expr_cell_hash, expr_cell_eqp> expr_cell_set;
+typedef std::unordered_set<expr_cell_offset, expr_cell_offset_hash, expr_cell_offset_eqp> expr_cell_offset_set;
 // =======================================
 
 // =======================================