diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index f7599fdf72..6858a8c992 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -50,6 +50,7 @@ meta inductive expr
 | elet  : name → expr → expr → expr → expr
 | lit   : literal → expr
 | mdata : lean.kvmap → expr → expr
+| proj  : nat → expr → expr
 | macro : macro_def → list expr → expr
 | quote : bool → expr → expr
 
@@ -341,6 +342,7 @@ meta def to_raw_fmt : expr → format
 | (pi n bi e t) := p ["pi", to_fmt n, repr bi, to_raw_fmt e, to_raw_fmt t]
 | (elet n g e f) := p ["elet", to_fmt n, to_raw_fmt g, to_raw_fmt e, to_raw_fmt f]
 | (mdata d e) := p ["mdata", to_raw_fmt e]
+| (proj idx e) := p ["proj", to_fmt idx, to_raw_fmt e]
 | (macro d args) := sbracket (format.join (list.intersperse " " ("macro" :: to_fmt (macro_def_name d) :: args.map to_raw_fmt)))
 | (quote b v) := p ["quote", to_fmt b, to_raw_fmt v]
 
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 23198798ce..99fcfa595a 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -972,6 +972,7 @@ expr elaborator::visit_function(expr const & fn, bool has_args, optional<expr> c
     case expr_kind::MData:     r = visit_mdata(fn, expected_type, true); break;
     case expr_kind::Lambda:    r = visit_lambda(fn, expected_type); break;
     case expr_kind::Let:       r = visit_let(fn, expected_type); break;
+    case expr_kind::Proj:      throw elaborator_exception(ref, "unexpected occurrence of proj constructor");
     case expr_kind::Quote:
         throw elaborator_exception(ref, "invalid application, function expected");
     }
@@ -3656,6 +3657,8 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
                     lean_unreachable();
                 case expr_kind::MData:
                     return copy_pos(e, visit_mdata(e, expected_type, false));
+                case expr_kind::Proj:
+                    throw elaborator_exception(e, "unexpected occurrence of proj constructor");
                 case expr_kind::Sort:
                     return copy_pos(e, visit_sort(e));
                 case expr_kind::FVar:
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 4c42342e76..095cd8a627 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -279,6 +279,8 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
         return save_pos(copy(e), p);
     case expr_kind::MData:
         return save_pos(::lean::mk_mdata(mdata_data(e), copy_with_new_pos(mdata_expr(e), p)), p);
+    case expr_kind::Proj:
+        return save_pos(::lean::mk_proj(proj_idx(e), copy_with_new_pos(proj_expr(e), p)), p);
     case expr_kind::App:
         return save_pos(::lean::mk_app(copy_with_new_pos(app_fn(e), p),
                                        copy_with_new_pos(app_arg(e), p)),
@@ -1762,6 +1764,8 @@ static expr quote(expr const & e) {
     case expr_kind::Let:
         return mk_app(mk_constant({"expr", "elet"}), mk_expr_placeholder(), quote(let_type(e)),
                       quote(let_value(e)), quote(let_body(e)));
+    case expr_kind::Proj:
+        return mk_app(mk_constant({"expr", "proj"}), quote(proj_idx(e).get_small_value()), quote(proj_expr(e)));
     case expr_kind::MData:
         if (is_antiquote(e))
             return get_antiquote_expr(e);
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index a092de1e89..ad3da60514 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1160,6 +1160,12 @@ auto pretty_fn::pp_mdata(expr const & e) -> result {
     }
 }
 
+auto pretty_fn::pp_proj(expr const & e) -> result {
+    format arg_fmt = pp_child(proj_expr(e), max_bp()).fmt();
+    format idx_fmt(proj_idx(e).get_small_value());
+    return result(arg_fmt + format(".") + idx_fmt);
+}
+
 auto pretty_fn::pp_let(expr e) -> result {
     buffer<std::tuple<expr, expr, expr>> decls;
     while (true) {
@@ -1771,6 +1777,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
     case expr_kind::FVar:      return pp_local(e);
     case expr_kind::Sort:      return pp_sort(e);
     case expr_kind::MData:     return pp_mdata(e);
+    case expr_kind::Proj:      return pp_proj(e);
     case expr_kind::Constant:  return pp_const(e);
     case expr_kind::MVar:      return pp_meta(e);
     case expr_kind::App:       return pp_app(e);
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index ddd0a833fd..2238448e26 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -153,6 +153,7 @@ private:
     result pp_explicit(expr const & e);
     result pp_delayed_abstraction(expr const & e);
     result pp_let(expr e);
+    result pp_proj(expr const & e);
     result pp_mdata(expr const & e);
     result pp_num(mpz const & n, unsigned bp);
     result pp_prod(expr const & e);
diff --git a/src/kernel/equiv_manager.cpp b/src/kernel/equiv_manager.cpp
index aef6842497..31115cdfee 100644
--- a/src/kernel/equiv_manager.cpp
+++ b/src/kernel/equiv_manager.cpp
@@ -96,7 +96,10 @@ bool equiv_manager::is_equiv_core(expr const & a, expr const & b) {
         result = lit_value(a) == lit_value(b);
         break;
     case expr_kind::MData:
-        result = mdata_expr(a) == mdata_expr(b);
+        result = is_equiv_core(mdata_expr(a), mdata_expr(b));
+        break;
+    case expr_kind::Proj:
+        result = is_equiv_core(proj_expr(a), proj_expr(b)) && proj_idx(a) == proj_idx(b);
         break;
     case expr_kind::Let:
         result =
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 43b646378d..702ced3fb3 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -319,6 +319,26 @@ void expr_mdata::dealloc(buffer<expr_cell*> & todelete) {
     delete this;
 }
 
+// Expr projections
+expr_proj::expr_proj(nat const & idx, expr const & e):
+    expr_composite(expr_kind::Proj, e.hash(),
+                   e.has_expr_metavar(),
+                   e.has_univ_metavar(),
+                   e.has_fvar(),
+                   e.has_param_univ(),
+                   inc_weight(get_weight(e)),
+                   get_loose_bvar_range(e)),
+    m_idx(idx), m_expr(e) {
+    m_depth = get_depth(e) + 1;
+    m_hash  = ::lean::hash(m_hash, m_weight);
+    m_hash  = ::lean::hash(m_hash, m_depth);
+}
+
+void expr_proj::dealloc(buffer<expr_cell*> & todelete) {
+    dec_ref(m_expr,  todelete);
+    delete this;
+}
+
 // Let expressions
 expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b):
     expr_composite(expr_kind::Let,
@@ -385,6 +405,9 @@ expr mk_metavar(name const & n, expr const & t) {
 expr mk_mdata(kvmap const & d, expr const & e) {
     return expr(new expr_mdata(d, e));
 }
+expr mk_proj(nat const & idx, expr const & e) {
+    return expr(new expr_proj(idx, e));
+}
 expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi) {
     return expr(new expr_fvar(n, pp_n, t, bi));
 }
@@ -421,6 +444,7 @@ void expr_cell::dealloc() {
             switch (it->kind()) {
             case expr_kind::Lit:        static_cast<expr_lit*>(it)->dealloc(); break;
             case expr_kind::MData:      static_cast<expr_mdata*>(it)->dealloc(todo); break;
+            case expr_kind::Proj:       static_cast<expr_proj*>(it)->dealloc(todo); break;
             case expr_kind::BVar:       static_cast<expr_bvar*>(it)->dealloc(); break;
             case expr_kind::MVar:       static_cast<expr_mlocal*>(it)->dealloc(todo); break;
             case expr_kind::FVar:       static_cast<expr_fvar*>(it)->dealloc(todo); break;
@@ -550,7 +574,7 @@ unsigned get_weight(expr const & e) {
         return 1;
     case expr_kind::Lambda: case expr_kind::Pi:
     case expr_kind::App:    case expr_kind::Let:
-    case expr_kind::MData:
+    case expr_kind::MData:  case expr_kind::Proj:
         return static_cast<expr_composite*>(e.raw())->m_weight;
 
 
@@ -569,7 +593,7 @@ unsigned get_depth(expr const & e) {
         return 1;
     case expr_kind::Lambda: case expr_kind::Pi:
     case expr_kind::App:    case expr_kind::Let:
-    case expr_kind::MData:
+    case expr_kind::MData:  case expr_kind::Proj:
         return static_cast<expr_composite*>(e.raw())->m_depth;
 
 
@@ -588,6 +612,13 @@ expr update_mdata(expr const & e, expr const & t) {
         return e;
 }
 
+expr update_proj(expr const & e, expr const & t) {
+    if (!is_eqp(proj_expr(e), t))
+        return mk_proj(proj_idx(e), t);
+    else
+        return e;
+}
+
 expr update_app(expr const & e, expr const & new_fn, expr const & new_arg) {
     if (!is_eqp(app_fn(e), new_fn) || !is_eqp(app_arg(e), new_arg))
         return mk_app(new_fn, new_arg);
@@ -658,7 +689,7 @@ bool is_atomic(expr const & e) {
     case expr_kind::App:      case expr_kind::MVar:
     case expr_kind::FVar:     case expr_kind::Lambda:
     case expr_kind::Pi:       case expr_kind::Let:
-    case expr_kind::MData:
+    case expr_kind::MData:    case expr_kind::Proj:
         return false;
 
 
@@ -813,6 +844,7 @@ unsigned hash_bi(expr const & e) {
 std::ostream & operator<<(std::ostream & out, expr_kind const & k) {
     switch (k) {
     case expr_kind::MData:    out << "MData"; break;
+    case expr_kind::Proj:     out << "Proj"; break;
     case expr_kind::Lit:      out << "Lit"; break;
     case expr_kind::BVar:     out << "BVar"; break;
     case expr_kind::FVar:     out << "FVar"; break;
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 7b19650228..d56ef7b38b 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -42,13 +42,14 @@ class expr;
           |   Let           name expr expr expr
           |   Lit           literal
           |   MData         kvmap expr
+          |   Proj          nat expr
 
           The following constructors will be deleted in the future
 
           |   Quote         bool expr
           |   Macro         macro
 */
-enum class expr_kind { BVar, FVar, Sort, Constant, MVar, App, Lambda, Pi, Let, Lit, MData, Macro, Quote };
+enum class expr_kind { BVar, FVar, Sort, Constant, MVar, App, Lambda, Pi, Let, Lit, MData, Proj, Macro, Quote };
 class expr_cell {
 protected:
     // The bits of the following field mean:
@@ -136,8 +137,8 @@ public:
     friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b);
     friend expr mk_lit(literal const & lit);
     friend expr mk_mdata(kvmap const & m, expr const & e);
+    friend expr mk_proj(nat const & idx, expr const & e);
     friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
-
     // TODO(Leo): delete
     friend expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi);
     friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args);
@@ -381,6 +382,18 @@ public:
     expr const & get_expr() const { return m_expr; }
 };
 
+class expr_proj : public expr_composite {
+    nat  m_idx;
+    expr m_expr;
+    friend expr_cell;
+    void dealloc(buffer<expr_cell*> & todelete);
+public:
+    expr_proj(nat const & idx, expr const & e);
+    ~expr_proj() {}
+    nat const & get_idx() const { return m_idx; }
+    expr const & get_expr() const { return m_expr; }
+};
+
 // =======================================
 // Testers
 inline bool is_bvar(expr_ptr e)        { return e->kind() == expr_kind::BVar; }
@@ -394,6 +407,7 @@ inline bool is_let(expr_ptr e)         { return e->kind() == expr_kind::Let; }
 inline bool is_sort(expr_ptr e)        { return e->kind() == expr_kind::Sort; }
 inline bool is_lit(expr_ptr e)         { return e->kind() == expr_kind::Lit; }
 inline bool is_mdata(expr_ptr e)       { return e->kind() == expr_kind::MData; }
+inline bool is_proj(expr_ptr e)        { return e->kind() == expr_kind::Proj; }
 inline bool is_binding(expr_ptr e)     { return is_lambda(e) || is_pi(e); }
 
 bool is_atomic(expr const & e);
@@ -406,6 +420,8 @@ bool is_metavar_app(expr const & e);
 // Constructors
 expr mk_lit(literal const & lit);
 expr mk_mdata(kvmap const & d, expr const & e);
+expr mk_proj(nat const & idx, expr const & e);
+inline expr mk_proj(unsigned idx, expr const & e) { return mk_proj(nat(idx), e); }
 expr mk_bvar(unsigned idx);
 expr mk_fvar(name const & n);
 inline expr BVar(unsigned idx) { return mk_bvar(idx); }
@@ -467,6 +483,7 @@ inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const
 // Casting (these functions are only needed for low-level code)
 inline expr_lit *         to_lit(expr_ptr e)        { lean_assert(is_lit(e));         return static_cast<expr_lit*>(e); }
 inline expr_mdata *       to_mdata(expr_ptr e)      { lean_assert(is_mdata(e));       return static_cast<expr_mdata*>(e); }
+inline expr_proj *        to_proj(expr_ptr e)       { lean_assert(is_proj(e));        return static_cast<expr_proj*>(e); }
 inline expr_bvar *        to_bvar(expr_ptr e)       { lean_assert(is_bvar(e));        return static_cast<expr_bvar*>(e); }
 inline expr_fvar *        to_fvar(expr_ptr e)       { lean_assert(is_fvar(e));        return static_cast<expr_fvar*>(e); }
 inline expr_const *       to_constant(expr_ptr e)   { lean_assert(is_constant(e));    return static_cast<expr_const*>(e); }
@@ -486,6 +503,8 @@ inline literal const & lit_value(expr_ptr e)             { return to_lit(e)->get
 expr lit_type(expr_ptr e);
 inline expr const &    mdata_expr(expr_ptr e)            { return to_mdata(e)->get_expr(); }
 inline kvmap const &   mdata_data(expr_ptr e)            { return to_mdata(e)->get_data(); }
+inline expr const &    proj_expr(expr_ptr e)             { return to_proj(e)->get_expr(); }
+inline nat const &     proj_idx(expr_ptr e)              { return to_proj(e)->get_idx(); }
 inline unsigned        bvar_idx(expr_ptr e)              { return to_bvar(e)->get_vidx(); }
 inline bool            is_bvar(expr_ptr e, unsigned i)   { return is_bvar(e) && bvar_idx(e) == i; }
 inline name const &    fvar_name(expr_ptr e)             { return to_fvar(e)->get_name(); }
@@ -576,6 +595,7 @@ expr update_sort(expr const & e, level const & new_level);
 expr update_constant(expr const & e, levels const & new_levels);
 expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body);
 expr update_mdata(expr const & e, expr const & t);
+expr update_proj(expr const & e, expr const & t);
 // =======================================
 
 
diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
index 193bd1387c..01c207d42d 100644
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -76,6 +76,10 @@ class expr_eq_fn {
             return
                 apply(mdata_expr(a), mdata_expr(b)) &&
                 mdata_data(a) == mdata_data(b);
+        case expr_kind::Proj:
+            return
+                apply(proj_expr(a), proj_expr(b)) &&
+                proj_idx(a) == proj_idx(b);
         case expr_kind::Lit:
             return lit_value(a) == lit_value(b);
         case expr_kind::Constant:
diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp
index eaa132f4cc..ac22d3e8c4 100644
--- a/src/kernel/for_each_fn.cpp
+++ b/src/kernel/for_each_fn.cpp
@@ -91,6 +91,9 @@ class for_each_fn {
             case expr_kind::MData:
                 todo.emplace_back(mdata_expr(e), offset);
                 goto begin_loop;
+            case expr_kind::Proj:
+                todo.emplace_back(proj_expr(e), offset);
+                goto begin_loop;
             case expr_kind::FVar:
                 // TODO(Leo): delete after refactoring
                 todo.emplace_back(mlocal_type(e), offset);
diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp
index 9ef7f0eea6..b769f1d4ff 100644
--- a/src/kernel/old_type_checker.cpp
+++ b/src/kernel/old_type_checker.cpp
@@ -225,6 +225,7 @@ expr old_type_checker::infer_type_core(expr const & e, bool infer_only) {
         if (!infer_only) check_level(sort_level(e));
         r = mk_sort(mk_succ(sort_level(e)));
         break;
+    case expr_kind::Proj: lean_unreachable();
     case expr_kind::MData:     r = infer_type_core(mdata_expr(e), infer_only); break;
     case expr_kind::Constant:  r = infer_constant(e, infer_only);       break;
     case expr_kind::Macro:     r = infer_macro(e, infer_only);          break;
@@ -290,6 +291,7 @@ expr old_type_checker::whnf_core(expr const & e) {
         return e;
     case expr_kind::MData:
         return whnf_core(mdata_expr(e));
+    case expr_kind::Proj: lean_unreachable();
     case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
         break;
     case expr_kind::Quote: throw_found_quote(m_env);
@@ -306,8 +308,8 @@ expr old_type_checker::whnf_core(expr const & e) {
     expr r;
     switch (e.kind()) {
     case expr_kind::BVar:  case expr_kind::Sort:    case expr_kind::MVar:   case expr_kind::FVar:
-    case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda: case expr_kind::Lit:
-    case expr_kind::MData:
+    case expr_kind::Pi:    case expr_kind::Constant: case expr_kind::Lambda: case expr_kind::Lit:
+    case expr_kind::MData: case expr_kind::Proj:
         lean_unreachable(); // LCOV_EXCL_LINE
     case expr_kind::Macro:
         if (auto m = expand_macro(e))
@@ -398,6 +400,8 @@ expr old_type_checker::whnf(expr const & e) {
         return e;
     case expr_kind::MData:
         return whnf(mdata_expr(e));
+    case expr_kind::Proj:
+        lean_unreachable();
     case expr_kind::Lambda:   case expr_kind::Macro: case expr_kind::App:
     case expr_kind::Constant: case expr_kind::Let:
         break;
@@ -498,6 +502,8 @@ lbool old_type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use
         case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let:
             // We do not handle these cases in this method.
             break;
+        case expr_kind::Proj:
+            lean_unreachable();
         case expr_kind::Lit:
             return to_lbool(lit_value(t) == lit_value(s));
         case expr_kind::Quote:
diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index 15ba4206e9..57df8eaa37 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -86,6 +86,10 @@ class replace_rec_fn {
                 expr new_e = apply(mdata_expr(e), offset);
                 return save_result(e, offset, update_mdata(e, new_e), shared);
             }
+            case expr_kind::Proj: {
+                expr new_e = apply(proj_expr(e), offset);
+                return save_result(e, offset, update_proj(e, new_e), shared);
+            }
             case expr_kind::MVar: {
                 expr new_t = apply(mlocal_type(e), offset);
                 return save_result(e, offset, update_mlocal(e, new_t), shared);
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 8a9886c081..ceabda1f45 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -201,6 +201,11 @@ expr type_checker::infer_let(expr const & _e, bool infer_only) {
     return m_lctx.mk_pi(fvars, r);
 }
 
+expr type_checker::infer_proj(expr const &, bool /* infer_only */) {
+    // TODO(Leo)
+    lean_unreachable();
+}
+
 /** \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.
     \pre closed(e) */
 expr type_checker::infer_type_core(expr const & e, bool infer_only) {
@@ -220,6 +225,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
     switch (e.kind()) {
     case expr_kind::Lit:       r = lit_type(e);    break;
     case expr_kind::MData:     r = infer_type_core(mdata_expr(e), infer_only); break;
+    case expr_kind::Proj:      r = infer_proj(e, infer_only); break;
     case expr_kind::FVar:      r = infer_fvar(e);  break;
     case expr_kind::MVar:      r = mlocal_type(e); break;
     case expr_kind::BVar:
@@ -297,6 +303,11 @@ expr type_checker::whnf_fvar(expr const & e) {
     return e;
 }
 
+optional<expr> type_checker::reduce_proj(expr const & /* e */) {
+    // TODO(Leo):
+    lean_unreachable();
+}
+
 /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
 expr type_checker::whnf_core(expr const & e) {
     check_system("whnf");
@@ -312,6 +323,7 @@ expr type_checker::whnf_core(expr const & e) {
     case expr_kind::FVar:
         return whnf_fvar(e);
     case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
+    case expr_kind::Proj:
         break;
 
     case expr_kind::Quote:
@@ -342,6 +354,14 @@ expr type_checker::whnf_core(expr const & e) {
         else
             r = e;
         break;
+
+    case expr_kind::Proj: {
+        if (auto m = reduce_proj(e))
+            r = whnf_core(*m);
+        else
+            r = e;
+        break;
+    }
     case expr_kind::App: {
         buffer<expr> args;
         expr f0 = get_app_rev_args(e, args);
@@ -427,7 +447,7 @@ expr type_checker::whnf(expr const & e) {
     case expr_kind::FVar:
         return whnf_fvar(e);
     case expr_kind::Lambda:   case expr_kind::Macro: case expr_kind::App:
-    case expr_kind::Constant: case expr_kind::Let:
+    case expr_kind::Constant: case expr_kind::Let:   case expr_kind::Proj:
         break;
 
     case expr_kind::Quote:
@@ -527,6 +547,7 @@ lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_has
             lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::BVar:      case expr_kind::FVar: case expr_kind::App:
         case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let:
+        case expr_kind::Proj:
             // We do not handle these cases in this method.
             break;
         case expr_kind::Lit:
@@ -730,6 +751,9 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
     if (is_fvar(t_n) && is_fvar(s_n) && fvar_name(t_n) == fvar_name(s_n))
         return true;
 
+    if (is_proj(t_n) && is_proj(s_n) && proj_idx(t_n) == proj_idx(s_n) && is_def_eq(proj_expr(t_n), proj_expr(s_n)))
+        return true;
+
     if (is_macro(t_n) && is_macro(s_n) && macro_def(t_n) == macro_def(s_n) && macro_num_args(t_n) == macro_num_args(s_n)) {
         unsigned i = 0;
         for (; i < macro_num_args(t_n); i++) {
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index e387f5c048..453c6ecaa8 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -51,12 +51,14 @@ class type_checker : public abstract_type_context {
     expr infer_lambda(expr const & e, bool infer_only);
     expr infer_pi(expr const & e, bool infer_only);
     expr infer_app(expr const & e, bool infer_only);
+    expr infer_proj(expr const & e, bool infer_only);
     expr infer_let(expr const & e, bool infer_only);
     expr infer_type_core(expr const & e, bool infer_only);
     expr infer_type(expr const & e);
 
     enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff };
     optional<expr> norm_ext(expr const & e);
+    optional<expr> reduce_proj(expr const & e);
     expr whnf_fvar(expr const & e);
     expr whnf_core(expr const & e);
     optional<declaration> is_delta(expr const & e) const;
diff --git a/src/library/check.cpp b/src/library/check.cpp
index f2fd296fce..a673563538 100644
--- a/src/library/check.cpp
+++ b/src/library/check.cpp
@@ -127,6 +127,8 @@ struct check_fn {
             return visit_let(e);
         case expr_kind::MData:
             return visit(mdata_expr(e));
+        case expr_kind::Proj:
+            return visit(proj_expr(e));
         case expr_kind::Macro:
             return visit_macro(e);
         case expr_kind::Quote:
diff --git a/src/library/compiler/cse.cpp b/src/library/compiler/cse.cpp
index 5f1bba6010..c0defb7a47 100644
--- a/src/library/compiler/cse.cpp
+++ b/src/library/compiler/cse.cpp
@@ -58,6 +58,7 @@ class cse_fn : public compiler_step_visitor {
             case expr_kind::App:      visit_app(e); break;
             case expr_kind::Let:      visit_let(e); break;
             case expr_kind::MData:    visit(mdata_expr(e)); break;
+            case expr_kind::Proj:     visit(proj_expr(e)); break;
             case expr_kind::Quote:
                 break;
             }
diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index 8e2120e24d..95826ee719 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -294,6 +294,10 @@ class vm_compiler_fn {
         }
     }
 
+    void compile_proj_cnstr(expr const & /* e */, unsigned /* bpz */, name_map<unsigned> const & /* m */) {
+        lean_unreachable();
+    }
+
     void compile(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
         switch (e.kind()) {
         case expr_kind::BVar:     lean_unreachable();
@@ -303,6 +307,7 @@ class vm_compiler_fn {
         case expr_kind::Lambda:   lean_unreachable();
         case expr_kind::Macro:    compile_macro(e, bpz, m);  break;
         case expr_kind::MData:    compile(mdata_expr(e), bpz, m); break;
+        case expr_kind::Proj:     compile_proj_cnstr(e, bpz, m);  break;
         case expr_kind::Constant: compile_constant(e);       break;
         case expr_kind::FVar:     compile_local(e, m);       break;
         case expr_kind::App:      compile_app(e, bpz, m);    break;
diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp
index 655bd633a2..7ce57f8e35 100644
--- a/src/library/deep_copy.cpp
+++ b/src/library/deep_copy.cpp
@@ -13,6 +13,7 @@ expr copy(expr const & a) {
     switch (a.kind()) {
     case expr_kind::Lit:      return mk_lit(lit_value(a));
     case expr_kind::MData:    return mk_mdata(mdata_data(a), mdata_expr(a));
+    case expr_kind::Proj:     return mk_proj(proj_idx(a), proj_expr(a));
     case expr_kind::BVar:     return mk_var(var_idx(a));
     case expr_kind::FVar:     return mk_local(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a), local_info(a));
     case expr_kind::Constant: return mk_constant(const_name(a), const_levels(a));
diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp
index e879f469ed..8a4983ca36 100644
--- a/src/library/equations_compiler/structural_rec.cpp
+++ b/src/library/equations_compiler/structural_rec.cpp
@@ -153,6 +153,8 @@ struct structural_rec_fn {
             }
             case expr_kind::MData:
                 return check_rhs(mdata_expr(e));
+            case expr_kind::Proj:
+                return check_rhs(proj_expr(e));
             case expr_kind::Let:
                 if (!check_rhs(let_value(e))) {
                     return false;
diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp
index 65b73db911..55e25a4341 100644
--- a/src/library/expr_lt.cpp
+++ b/src/library/expr_lt.cpp
@@ -30,6 +30,11 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const *
             return is_lt(mdata_expr(a), mdata_expr(b), use_hash, lctx);
         else
             return mdata_data(a) < mdata_data(b);
+    case expr_kind::Proj:
+        if (proj_expr(a) != proj_expr(b))
+            return is_lt(proj_expr(a), proj_expr(b), use_hash, lctx);
+        else
+            return proj_idx(a) < proj_idx(b);
     case expr_kind::Constant:
         if (const_name(a) != const_name(b))
             return const_name(a) < const_name(b);
@@ -146,6 +151,11 @@ bool is_lt_no_level_params(expr const & a, expr const & b) {
             return is_lt_no_level_params(mdata_expr(a), mdata_expr(b));
         else
             return mdata_data(a) < mdata_data(b);
+    case expr_kind::Proj:
+        if (proj_expr(a) != proj_expr(b))
+            return is_lt_no_level_params(proj_expr(a), proj_expr(b));
+        else
+            return proj_idx(a) < proj_idx(b);
     case expr_kind::Constant:
         if (const_name(a) != const_name(b))
             return const_name(a) < const_name(b);
diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index 0814133434..432cb9683e 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -535,6 +535,7 @@ class add_nested_inductive_decl_fn {
         case expr_kind::Quote:
         case expr_kind::Lit:
         case expr_kind::MData:
+        case expr_kind::Proj:
             return _e;
         case expr_kind::Lambda:
         case expr_kind::Pi:
@@ -592,6 +593,7 @@ class add_nested_inductive_decl_fn {
         case expr_kind::Quote:
         case expr_kind::Lit:
         case expr_kind::MData:
+        case expr_kind::Proj:
             return _e;
         case expr_kind::Lambda:
         case expr_kind::Pi:
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index 05ee7126c5..48a293648a 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -65,6 +65,10 @@ class expr_serializer : public object_serializer<expr, expr_hash, is_bi_equal_pr
                     s << mdata_data(a);
                     write_core(mdata_expr(a));
                     break;
+                case expr_kind::Proj:
+                    s << proj_idx(a);
+                    write_core(proj_expr(a));
+                    break;
                 case expr_kind::Constant:
                     lean_assert(!const_name(a).is_anonymous());
                     s << const_name(a) << const_levels(a);
@@ -139,6 +143,10 @@ public:
                     kvmap m = read_list_ref<pair_ref<name, data_value>>(d);
                     return mk_mdata(m, read());
                 }
+                case expr_kind::Proj: {
+                    nat idx = read_nat(d);
+                    return mk_proj(idx, read());
+                }
                 case expr_kind::Constant: {
                     auto n = read_name(d);
                     return mk_constant(n, read_levels(d));
diff --git a/src/library/locals.cpp b/src/library/locals.cpp
index d64c07652e..ded82a66cd 100644
--- a/src/library/locals.cpp
+++ b/src/library/locals.cpp
@@ -78,6 +78,9 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
         case expr_kind::MData:
             visit(mdata_expr(e));
             break;
+        case expr_kind::Proj:
+            visit(proj_expr(e));
+            break;
         case expr_kind::FVar:
             if (!restricted)
                 visit(mlocal_type(e));
diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index 615d333929..d20d804479 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -67,6 +67,11 @@ struct max_sharing_fn::imp {
             res = update_mdata(a, new_e);
             break;
         }
+        case expr_kind::Proj: {
+            expr new_e = apply(proj_expr(a));
+            res = update_proj(a, new_e);
+            break;
+        }
         case expr_kind::App: {
             expr new_f = apply(app_fn(a));
             expr new_a = apply(app_arg(a));
diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp
index 2848826408..df6a2e1a8a 100644
--- a/src/library/noncomputable.cpp
+++ b/src/library/noncomputable.cpp
@@ -209,6 +209,7 @@ struct get_noncomputable_reason_fn {
         case expr_kind::Pi:        visit_binding(e);  return;
         case expr_kind::Let:       visit_let(e);      return;
         case expr_kind::MData:     visit_mdata(e);    return;
+        case expr_kind::Proj:      visit(proj_expr(e)); return;
         case expr_kind::Quote:     return;
         }
     }
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 86f13dddef..fe2097c65c 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -121,6 +121,8 @@ class normalize_fn {
             return e;
         case expr_kind::MData:
             lean_unreachable();
+        case expr_kind::Proj:
+            lean_unreachable();
         case expr_kind::Lambda: {
             e = normalize_binding(e);
             if (m_use_eta)
diff --git a/src/library/pos_info_provider.cpp b/src/library/pos_info_provider.cpp
index 54a237a885..a4da43fe47 100644
--- a/src/library/pos_info_provider.cpp
+++ b/src/library/pos_info_provider.cpp
@@ -147,6 +147,10 @@ class replace_rec_fn2 {
                 expr new_e = apply(mdata_expr(e), offset);
                 return save_result(e, offset, copy_pos(e, update_mdata(e, new_e)), shared);
             }
+            case expr_kind::Proj: {
+                expr new_e = apply(proj_expr(e), offset);
+                return save_result(e, offset, copy_pos(e, update_proj(e, new_e)), shared);
+            }
             case expr_kind::App: {
                 expr new_f = apply(app_fn(e), offset);
                 expr new_a = apply(app_arg(e), offset);
diff --git a/src/library/print.cpp b/src/library/print.cpp
index 78b85418b4..7070a93ef5 100644
--- a/src/library/print.cpp
+++ b/src/library/print.cpp
@@ -225,6 +225,9 @@ struct print_expr_fn {
         case expr_kind::MData:
             out() << "[mdata "; print(mdata_expr(a)); out() << "]";
             break;
+        case expr_kind::Proj:
+            print(proj_expr(a)); out() << "." << proj_idx(a).to_mpz();
+            break;
         case expr_kind::BVar:
             out() << "#" << var_idx(a);
             break;
diff --git a/src/library/replace_visitor.cpp b/src/library/replace_visitor.cpp
index bd2d490ae2..3291b1e4ac 100644
--- a/src/library/replace_visitor.cpp
+++ b/src/library/replace_visitor.cpp
@@ -27,6 +27,9 @@ expr replace_visitor::visit_local(expr const & e) { return visit_mlocal(e); }
 expr replace_visitor::visit_mdata(expr const & e) {
     return update_mdata(e, visit(mdata_expr(e)));
 }
+expr replace_visitor::visit_proj(expr const & e) {
+    return update_proj(e, visit(proj_expr(e)));
+}
 expr replace_visitor::visit_app(expr const & e) {
     lean_assert(is_app(e));
     expr new_fn  = visit(app_fn(e));
@@ -73,6 +76,7 @@ expr replace_visitor::visit(expr const & e) {
     switch (e.kind()) {
     case expr_kind::Lit:       return save_result(e, visit_lit(e), shared);
     case expr_kind::MData:     return save_result(e, visit_mdata(e), shared);
+    case expr_kind::Proj:      return save_result(e, visit_proj(e), shared);
     case expr_kind::Sort:      return save_result(e, visit_sort(e), shared);
     case expr_kind::Constant:  return save_result(e, visit_constant(e), shared);
     case expr_kind::BVar:      return save_result(e, visit_var(e), shared);
diff --git a/src/library/replace_visitor.h b/src/library/replace_visitor.h
index b0cb3d1f19..48625a909d 100644
--- a/src/library/replace_visitor.h
+++ b/src/library/replace_visitor.h
@@ -31,6 +31,7 @@ protected:
     virtual expr visit_let(expr const & e);
     virtual expr visit_lit(expr const & e);
     virtual expr visit_mdata(expr const & e);
+    virtual expr visit_proj(expr const & e);
     virtual expr visit(expr const &);
 
     virtual expr visit_macro(expr const &);
diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp
index 0ef041e9b8..b46958bbfb 100644
--- a/src/library/tactic/dsimplify.cpp
+++ b/src/library/tactic/dsimplify.cpp
@@ -263,6 +263,9 @@ expr dsimplify_core_fn::visit(expr const & e) {
         case expr_kind::MData:
             new_e = mdata_expr(curr_e);
             break;
+        case expr_kind::Proj:
+            new_e = curr_e;
+            break;
         case expr_kind::BVar:
             lean_unreachable();
         case expr_kind::MVar:
diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
index 420d6567e4..ff79a6f74f 100644
--- a/src/library/tactic/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -647,6 +647,8 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset,
         }
     case expr_kind::MData:
         return is_permutation(mdata_expr(lhs), mdata_expr(rhs), offset, p);
+    case expr_kind::Proj:
+        return proj_idx(lhs) == proj_idx(rhs) && is_permutation(proj_expr(lhs), proj_expr(rhs), offset, p);
     case expr_kind::Lambda: case expr_kind::Pi:
         return
             is_permutation(binding_domain(lhs), binding_domain(rhs), offset, p) &&
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index d458d4e830..0e4174d852 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -671,6 +671,9 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
         case expr_kind::MData:
             new_result = join(curr_result, visit(mdata_expr(e), some_expr(e)));
             break;
+        case expr_kind::Proj:
+            new_result = curr_result;
+            break;
         case expr_kind::Macro:
             new_result = join(curr_result, visit_macro(curr_result.get_new()));
             break;
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 2797eb198d..61831657db 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -676,6 +676,11 @@ optional<expr> type_context_old::reduce_projection(expr const & e) {
     return reduce_projection_core(info, e);
 }
 
+optional<expr> type_context_old::reduce_proj(expr const & /* e */) {
+    // TODO(Leo):
+    lean_unreachable();
+}
+
 optional<expr> type_context_old::reduce_aux_recursor(expr const & e) {
     expr const & f = get_app_fn(e);
     if (!is_constant(f))
@@ -860,6 +865,12 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
             continue;
         }
     }
+    case expr_kind::Proj:
+        if (auto r = reduce_proj(e)) {
+            e = *r;
+            continue;
+        }
+        return e;
     case expr_kind::MData:
         e = mdata_expr(e);
         continue;
@@ -980,6 +991,11 @@ expr type_context_old::infer(expr const & e) {
     return infer_core(e);
 }
 
+expr type_context_old::infer_proj(expr const & e) {
+    // TODO(Leo):
+    lean_unreachable();
+}
+
 expr type_context_old::infer_core(expr const & e) {
     if (auto r = m_cache->get_infer(e))
         return *r;
@@ -1000,6 +1016,9 @@ expr type_context_old::infer_core(expr const & e) {
     case expr_kind::MData:
         r = infer_core(mdata_expr(e));
         break;
+    case expr_kind::Proj:
+        r = infer_proj(e);
+        break;
     case expr_kind::BVar:
         throw exception("failed to infer type, unexpected bound variable occurrence");
     case expr_kind::Sort:
@@ -2709,7 +2728,7 @@ lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) {
             return to_lbool(lit_value(e1) == lit_value(e2));
         case expr_kind::MVar:     case expr_kind::BVar:
         case expr_kind::FVar:     case expr_kind::App:
-        case expr_kind::Constant:
+        case expr_kind::Constant: case expr_kind::Proj:
         case expr_kind::Let:
             // We do not handle these cases in this method.
             break;
@@ -3337,6 +3356,8 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
             return l_false;
         case expr_kind::Let:
             return l_undef;
+        case expr_kind::Proj:
+            return l_undef;
         case expr_kind::MData:
             it = &mdata_expr(*it);
             break;
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 9eecc847fb..0ef8d71000 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -685,6 +685,7 @@ public:
     optional<expr> reduce_aux_recursor(expr const & e);
     optional<expr> reduce_large_elim_recursor(expr const & e);
     optional<expr> reduce_projection(expr const & e);
+    optional<expr> reduce_proj(expr const & e);
     optional<expr> norm_ext(expr const & e);
     optional<expr> reduce_recursor(expr const & e);
 
@@ -933,6 +934,7 @@ private:
     level get_level(expr const & A);
     expr infer_pi(expr e);
     expr infer_app(expr const & e);
+    expr infer_proj(expr const & e);
     expr infer_let(expr e);
 
 public:
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index 31d8311153..f920f821a6 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -243,6 +243,10 @@ unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
         data.push_back(to_obj(mdata_data(e)));
         data.push_back(to_obj(mdata_expr(e)));
         break;
+    case expr_kind::Proj:
+        data.push_back(to_obj(proj_idx(e)));
+        data.push_back(to_obj(proj_expr(e)));
+        break;
     case expr_kind::Macro: {
         data.push_back(to_obj(macro_def(e)));
         buffer<expr> args;
diff --git a/src/util/nat.h b/src/util/nat.h
index a4f12b2d14..b2411a755c 100644
--- a/src/util/nat.h
+++ b/src/util/nat.h
@@ -48,5 +48,10 @@ public:
     friend nat operator*(nat const & a, nat const & b) { return wrap(nat_mul(a.raw(), b.raw())); }
     friend nat operator/(nat const & a, nat const & b) { return wrap(nat_div(a.raw(), b.raw())); }
     friend nat operator%(nat const & a, nat const & b) { return wrap(nat_mod(a.raw(), b.raw())); }
+    void serialize(serializer & s) const { s.write_object(raw()); }
 };
+
+inline serializer & operator<<(serializer & s, nat const & n) { n.serialize(s); return s; }
+inline nat read_nat(deserializer & d) { return nat(d.read_object()); }
+inline deserializer & operator>>(deserializer & d, nat & n) { n = read_nat(d); return d; }
 };