diff --git a/library/init/core.lean b/library/init/core.lean
index 61c5fafc36..bda491050e 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -215,20 +215,18 @@ intro :: (mp : a → b) (mpr : b → a)
 
 infix = := eq
 
-attribute [refl] eq.refl
-
 @[pattern] def rfl {α : Sort u} {a : α} : a = a := eq.refl a
 
-@[elab_as_eliminator, subst]
+@[elab_as_eliminator]
 theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
 eq.ndrec h₂ h₁
 
 notation h1 ▸ h2 := eq.subst h1 h2
 
-@[trans] theorem eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
+theorem eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
 h₂ ▸ h₁
 
-@[symm] theorem eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
+theorem eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
 h ▸ rfl
 
 infix == := heq
@@ -627,7 +625,7 @@ notation x && y := band x y
 
 def implies (a b : Prop) := a → b
 
-@[trans] theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
+theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
 assume hp, h₂ (h₁ hp)
 
 def trivial : true := ⟨⟩
@@ -725,8 +723,6 @@ theorem eq_tt_of_ne_ff : ∀ {b : bool}, b ≠ ff → b = tt
 | tt h := rfl
 | ff h := false.elim (h rfl)
 
-attribute [refl] heq.refl
-
 section
 variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
 
@@ -744,19 +740,19 @@ eq.rec_on (eq_of_heq h₁) h₂
 theorem heq.subst {p : ∀ T : Sort u, T → Prop} (h₁ : a == b) (h₂ : p α a) : p β b :=
 heq.ndrec_on h₁ h₂
 
-@[symm] theorem heq.symm (h : a == b) : b == a :=
+theorem heq.symm (h : a == b) : b == a :=
 heq.ndrec_on h (heq.refl a)
 
 theorem heq_of_eq (h : a = a') : a == a' :=
 eq.subst h (heq.refl a)
 
-@[trans] theorem heq.trans (h₁ : a == b) (h₂ : b == c) : a == c :=
+theorem heq.trans (h₁ : a == b) (h₂ : b == c) : a == c :=
 heq.subst h₂ h₁
 
-@[trans] theorem heq_of_heq_of_eq (h₁ : a == b) (h₂ : b = b') : a == b' :=
+theorem heq_of_heq_of_eq (h₁ : a == b) (h₂ : b = b') : a == b' :=
 heq.trans h₁ (heq_of_eq h₂)
 
-@[trans] theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' == b) : a == b :=
+theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' == b) : a == b :=
 heq.trans (heq_of_eq h₁) h₂
 
 def type_eq_of_heq (h : a == b) : α = β :=
@@ -820,20 +816,17 @@ theorem iff.elim_right : (a ↔ b) → b → a := iff.mpr
 theorem iff_iff_implies_and_implies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
 iff.intro (λ h, and.intro h.mp h.mpr) (λ h, iff.intro h.left h.right)
 
-@[refl]
 theorem iff.refl (a : Prop) : a ↔ a :=
 iff.intro (assume h, h) (assume h, h)
 
 theorem iff.rfl {a : Prop} : a ↔ a :=
 iff.refl a
 
-@[trans]
 theorem iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
 iff.intro
   (assume ha, iff.mp h₂ (iff.mp h₁ ha))
   (assume hc, iff.mpr h₁ (iff.mpr h₂ hc))
 
-@[symm]
 theorem iff.symm (h : a ↔ b) : b ↔ a :=
 iff.intro (iff.elim_right h) (iff.elim_left h)
 
@@ -1734,15 +1727,15 @@ instance setoid_has_equiv {α : Sort u} [setoid α] : has_equiv α :=
 namespace setoid
 variables {α : Sort u} [setoid α]
 
-@[refl] theorem refl (a : α) : a ≈ a :=
+theorem refl (a : α) : a ≈ a :=
 match setoid.iseqv α with
 | ⟨h_refl, h_symm, h_trans⟩ := h_refl a
 
-@[symm] theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
+theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
 match setoid.iseqv α with
 | ⟨h_refl, h_symm, h_trans⟩ := h_symm hab
 
-@[trans] theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
+theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
 (match setoid.iseqv α with
  | ⟨h_refl, h_symm, h_trans⟩ := h_trans hab hbc)
 end setoid
@@ -1787,7 +1780,7 @@ eq.subst (@iff_eq_eq a true) this
 /- Quotients -/
 
 -- iff can now be used to do substitutions in a calculation
-@[subst] theorem iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
+theorem iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
 eq.subst (propext h₁) h₂
 
 namespace quot
diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean
index e642dd285f..3b952f555a 100644
--- a/library/init/data/nat/basic.lean
+++ b/library/init/data/nat/basic.lean
@@ -198,7 +198,7 @@ h₁ ◾ h₂ ◾ h₃ ◾ h₄ ◾ h₅ ◾ h₆
 
 /- Inequalities -/
 
-@[refl] protected def le_refl : ∀ n : nat, n ≤ n
+protected def le_refl : ∀ n : nat, n ≤ n
 | zero     := rfl
 | (succ n) := le_refl n
 
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index aaabfea095..c77d506bb5 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -6,8 +6,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   class.cpp util.cpp print.cpp annotation.cpp quote.cpp
   protected.cpp reducible.cpp init_module.cpp
   exception.cpp fingerprint.cpp pp_options.cpp
-  app_builder.cpp projection.cpp relation_manager.cpp
-  user_recursors.cpp idx_metavar.cpp noncomputable.cpp
+  app_builder.cpp projection.cpp user_recursors.cpp idx_metavar.cpp noncomputable.cpp
   aux_recursors.cpp trace.cpp
   attribute_manager.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp
   fun_info.cpp replace_visitor_with_tc.cpp aux_definition.cpp pattern_attribute.cpp
diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index 4c768c25b5..cba3ce8dfe 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -13,7 +13,6 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/cache_helper.h"
 #include "library/app_builder.h"
-#include "library/relation_manager.h"
 
 namespace lean {
 static void trace_fun(name const & n) {
@@ -414,26 +413,6 @@ public:
         return mk_app(c, total_nargs, {a1, a2, a3});
     }
 
-    /** \brief Similar to mk_app(n, lhs, rhs), but handles eq and iff more efficiently. */
-    expr mk_rel(name const & n, expr const & lhs, expr const & rhs) {
-        if (n == get_eq_name()) {
-            return mk_eq(lhs, rhs);
-        } else if (n == get_iff_name()) {
-            return mk_iff(lhs, rhs);
-        } else if (auto info = get_relation_info(env(), n)) {
-            buffer<bool> mask;
-            for (unsigned i = 0; i < info->get_arity(); i++) {
-                mask.push_back(i == info->get_lhs_pos() || i == info->get_rhs_pos());
-            }
-            expr args[2] = {lhs, rhs};
-            return mk_app(n, info->get_arity(), mask.data(), args);
-        } else {
-            // for unregistered relations assume lhs and rhs are the last two arguments.
-            expr args[2] = {lhs, rhs};
-            return mk_app(n, 2, args);
-        }
-    }
-
     expr mk_eq(expr const & a, expr const & b) {
         expr A    = m_ctx.infer(a);
         level lvl = get_level(A);
@@ -459,8 +438,6 @@ public:
             return mk_iff_refl(a);
         } else if (relname == get_heq_name()) {
             return mk_heq_refl(a);
-        } else if (auto info = get_refl_extra_info(env(), relname)) {
-            return mk_app(info->m_name, 1, &a);
         } else {
             lean_app_builder_trace(
                 tout() << "failed to build reflexivity proof, '" << relname
@@ -490,8 +467,6 @@ public:
             return mk_iff_symm(H);
         } else if (relname == get_heq_name()) {
             return mk_heq_symm(H);
-        } else if (auto info = get_symm_extra_info(env(), relname)) {
-            return mk_app(info->m_name, 1, &H);
         } else {
             lean_app_builder_trace(
                 tout() << "failed to build symmetry proof, '" << relname
@@ -544,9 +519,6 @@ public:
             return mk_iff_trans(H1, H2);
         } else if (relname == get_heq_name()) {
             return mk_heq_trans(H1, H2);
-        } else if (auto info = get_trans_extra_info(env(), relname, relname)) {
-            expr args[2] = {H1, H2};
-            return mk_app(info->m_name, 2, args);
         } else {
             lean_app_builder_trace(
                 tout() << "failed to build symmetry proof, '" << relname
@@ -670,27 +642,6 @@ public:
         return ::lean::mk_app({mk_constant(get_heq_of_eq_name(), {lvl}), A, a, b, H});
     }
 
-    /** \brief Given a reflexive relation R, and a proof H : a = b,
-        build a proof for (R a b) */
-    expr lift_from_eq(name const & R, expr const & H) {
-        if (R == get_eq_name())
-            return H;
-        expr H_type = m_ctx.relaxed_whnf(m_ctx.infer(H));
-        // H_type : @eq A a b
-        expr A, a, b;
-        if (!is_eq(H_type, A, a, b)) {
-            lean_app_builder_trace(tout() << "failed to build lift_of_eq equality proof expected:\n" << H << "\n";);
-            throw app_builder_exception();
-        }
-        type_context_old::tmp_locals locals(m_ctx);
-        expr x         = locals.push_local(name("A"), A);
-        // motive := fun x : A, a ~ x
-        expr motive    = locals.mk_lambda(mk_rel(R, a, x));
-        // minor : a ~ a
-        expr minor     = mk_refl(R, a);
-        return mk_eq_rec(motive, minor, H);
-    }
-
     expr mk_ss_elim(expr const & A, expr const & ss_inst, expr const & old_e, expr const & new_e) {
         level lvl = get_level(A);
         return ::lean::mk_app(mk_constant(get_subsingleton_elim_name(), {lvl}), A, ss_inst, old_e, new_e);
@@ -784,10 +735,6 @@ expr mk_app(type_context_old & ctx, name const & c, unsigned total_nargs, unsign
     return app_builder(ctx).mk_app(c, total_nargs, expl_nargs, expl_args);
 }
 
-expr mk_rel(type_context_old & ctx, name const & n, expr const & lhs, expr const & rhs) {
-    return app_builder(ctx).mk_rel(n, lhs, rhs);
-}
-
 expr mk_eq(type_context_old & ctx, expr const & lhs, expr const & rhs) {
     return app_builder(ctx).mk_eq(lhs, rhs);
 }
@@ -950,10 +897,6 @@ expr mk_funext(type_context_old & ctx, expr const & lam_pf) {
     return mk_app(ctx, get_funext_name(), lam_pf);
 }
 
-expr lift_from_eq(type_context_old & ctx, name const & R, expr const & H) {
-    return app_builder(ctx).lift_from_eq(R, H);
-}
-
 expr mk_iff_false_intro(type_context_old & ctx, expr const & H) {
     // TODO(Leo): implement custom version if bottleneck.
     return mk_app(ctx, get_iff_false_intro_name(), {H});
diff --git a/src/library/app_builder.h b/src/library/app_builder.h
index 9217d4850e..ccce73dabd 100644
--- a/src/library/app_builder.h
+++ b/src/library/app_builder.h
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include <memory>
 #include <unordered_map>
 #include "kernel/environment.h"
-#include "library/relation_manager.h"
 #include "library/reducible.h"
 #include "library/type_context.h"
 
@@ -81,7 +80,6 @@ inline expr mk_app(type_context_old & ctx, name const & c, unsigned total_nargs,
 }
 
 /** \brief Similar to mk_app(n, lhs, rhs), but handles eq and iff more efficiently. */
-expr mk_rel(type_context_old & ctx, name const & n, expr const & lhs, expr const & rhs);
 expr mk_eq(type_context_old & ctx, expr const & lhs, expr const & rhs);
 expr mk_iff(type_context_old & ctx, expr const & lhs, expr const & rhs);
 expr mk_heq(type_context_old & ctx, expr const & lhs, expr const & rhs);
@@ -133,10 +131,6 @@ expr mk_congr(type_context_old & ctx, expr const & H1, expr const & H2, bool ski
 
 expr mk_funext(type_context_old & ctx, expr const & lam_pf);
 
-/** \brief Given a reflexive relation R, and a proof H : a = b,
-    build a proof for (R a b) */
-expr lift_from_eq(type_context_old & ctx, name const & R, expr const & H);
-
 /** \brief not p -> (p <-> false) */
 expr mk_iff_false_intro(type_context_old & ctx, expr const & H);
 /** \brief p -> (p <-> true) */
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 5d41462de2..c785da0f96 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -27,7 +27,6 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/pp_options.h"
 #include "library/projection.h"
-#include "library/relation_manager.h"
 #include "library/user_recursors.h"
 #include "library/noncomputable.h"
 #include "library/aux_recursors.h"
@@ -98,7 +97,6 @@ void initialize_library_module() {
     initialize_quote();
     initialize_pp_options();
     initialize_projection();
-    initialize_relation_manager();
     initialize_user_recursors();
     initialize_noncomputable();
     initialize_aux_recursors();
@@ -126,7 +124,6 @@ void finalize_library_module() {
     finalize_aux_recursors();
     finalize_noncomputable();
     finalize_user_recursors();
-    finalize_relation_manager();
     finalize_projection();
     finalize_pp_options();
     finalize_quote();
diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp
deleted file mode 100644
index d2a0f86d28..0000000000
--- a/src/library/relation_manager.cpp
+++ /dev/null
@@ -1,351 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "runtime/sstream.h"
-#include "runtime/optional.h"
-#include "util/name.h"
-#include "util/rb_map.h"
-#include "library/constants.h"
-#include "library/scoped_ext.h"
-#include "library/relation_manager.h"
-#include "library/attribute_manager.h"
-
-namespace lean {
-// Check whether e is of the form (f ...) where f is a constant. If it is return f.
-static name const & get_fn_const(expr const & e, char const * msg) {
-    expr const & fn = get_app_fn(e);
-    if (!is_constant(unwrap_pos(fn)))
-        throw exception(msg);
-    return const_name(fn);
-}
-
-static pair<expr, unsigned> extract_arg_types_core(environment const & env, name const & f, buffer<expr> & arg_types) {
-    constant_info info = env.get(f);
-    expr f_type = info.get_type();
-    while (is_pi(f_type)) {
-        arg_types.push_back(binding_domain(f_type));
-        f_type = binding_body(f_type);
-    }
-    return mk_pair(f_type, info.get_num_lparams());
-}
-
-enum class op_kind { Relation, Subst, Trans, Refl, Symm };
-
-struct rel_entry {
-    op_kind m_kind;
-    name    m_name;
-    rel_entry() {}
-    rel_entry(op_kind k, name const & n):m_kind(k), m_name(n) {}
-};
-
-struct rel_state {
-    typedef name_map<refl_info> refl_table;
-    typedef name_map<subst_info> subst_table;
-    typedef name_map<symm_info> symm_table;
-    typedef rb_map<name_pair, trans_info, name_pair_quick_cmp> trans_table;
-    typedef name_map<relation_info> rop_table;
-    trans_table    m_trans_table;
-    refl_table     m_refl_table;
-    subst_table    m_subst_table;
-    symm_table     m_symm_table;
-    rop_table      m_rop_table;
-    rel_state() {}
-
-    bool is_equivalence(name const & rop) const {
-        return m_trans_table.contains(mk_pair(rop, rop)) && m_refl_table.contains(rop) && m_symm_table.contains(rop);
-    }
-
-    static void throw_invalid_relation(name const & rop) {
-        throw exception(sstream() << "invalid binary relation declaration, relation '" << rop
-                        << "' must have two explicit parameters");
-    }
-
-    void register_rop(environment const & env, name const & rop) {
-        if (m_rop_table.contains(rop))
-            return;
-        constant_info info = env.get(rop);
-        optional<unsigned> lhs_pos;
-        optional<unsigned> rhs_pos;
-        unsigned i = 0;
-        expr type = info.get_type();
-        while (is_pi(type)) {
-            if (is_explicit(binding_info(type))) {
-                if (!lhs_pos) {
-                    lhs_pos = i;
-                } else if (!rhs_pos) {
-                    rhs_pos = i;
-                } else {
-                    lhs_pos = rhs_pos;
-                    rhs_pos = i;
-                }
-            }
-            type = binding_body(type);
-            i++;
-        }
-        if (lhs_pos && rhs_pos) {
-            m_rop_table.insert(rop, relation_info(i, *lhs_pos, *rhs_pos));
-        } else {
-            throw_invalid_relation(rop);
-        }
-    }
-
-    void add_subst(environment const & env, name const & subst) {
-        buffer<expr> arg_types;
-        auto p          = extract_arg_types_core(env, subst, arg_types);
-        expr r_type     = p.first;
-        unsigned nunivs = p.second;
-        unsigned nargs  = arg_types.size();
-        if (nargs < 2)
-            throw exception("invalid substitution theorem, it must have at least 2 arguments");
-        name const & rop = get_fn_const(arg_types[nargs-2], "invalid substitution theorem, penultimate argument must be an operator application");
-        m_subst_table.insert(rop, subst_info(subst, nunivs, nargs));
-    }
-
-    void add_refl(environment const & env, name const & refl) {
-        buffer<expr> arg_types;
-        auto p          = extract_arg_types_core(env, refl, arg_types);
-        expr r_type     = p.first;
-        unsigned nunivs = p.second;
-        unsigned nargs  = arg_types.size();
-        if (nargs < 1)
-            throw exception("invalid reflexivity rule, it must have at least 1 argument");
-        name const & rop = get_fn_const(r_type, "invalid reflexivity rule, result type must be an operator application");
-        register_rop(env, rop);
-        m_refl_table.insert(rop, refl_info(refl, nunivs, nargs));
-    }
-
-    void add_trans(environment const & env, name const & trans) {
-        buffer<expr> arg_types;
-        auto p = extract_arg_types_core(env, trans, arg_types);
-        expr r_type     = p.first;
-        unsigned nunivs = p.second;
-        unsigned nargs  = arg_types.size();
-        if (nargs < 5)
-            throw exception("invalid transitivity rule, it must have at least 5 arguments");
-        name const & rop = get_fn_const(r_type, "invalid transitivity rule, result type must be an operator application");
-        name const & op1 = get_fn_const(arg_types[nargs-2], "invalid transitivity rule, penultimate argument must be an operator application");
-        name const & op2 = get_fn_const(arg_types[nargs-1], "invalid transitivity rule, last argument must be an operator application");
-        register_rop(env, rop);
-        m_trans_table.insert(name_pair(op1, op2), trans_info(trans, nunivs, nargs, rop));
-    }
-
-    void add_symm(environment const & env, name const & symm) {
-        buffer<expr> arg_types;
-        auto p          = extract_arg_types_core(env, symm, arg_types);
-        expr r_type     = p.first;
-        unsigned nunivs = p.second;
-        unsigned nargs  = arg_types.size();
-        if (nargs < 1)
-            throw exception("invalid symmetry rule, it must have at least 1 argument");
-        name const & rop = get_fn_const(r_type, "invalid symmetry rule, result type must be an operator application");
-        register_rop(env, rop);
-        m_symm_table.insert(rop, symm_info(symm, nunivs, nargs));
-    }
-};
-
-struct rel_config {
-    typedef rel_state state;
-    typedef rel_entry entry;
-    static void add_entry(environment const & env, io_state const &, state & s, entry const & e) {
-        switch (e.m_kind) {
-        case op_kind::Relation: s.register_rop(env, e.m_name); break;
-        case op_kind::Refl:     s.add_refl(env, e.m_name); break;
-        case op_kind::Subst:    s.add_subst(env, e.m_name); break;
-        case op_kind::Trans:    s.add_trans(env, e.m_name); break;
-        case op_kind::Symm:     s.add_symm(env, e.m_name); break;
-        }
-    }
-    static const char * get_serialization_key() { return "REL"; }
-    static void  write_entry(serializer & s, entry const & e) {
-        s << static_cast<char>(e.m_kind) << e.m_name;
-    }
-    static entry read_entry(deserializer & d) {
-        entry e;
-        char cmd;
-        d >> cmd >> e.m_name;
-        e.m_kind = static_cast<op_kind>(cmd);
-        return e;
-    }
-    static optional<unsigned> get_fingerprint(entry const &) {
-        return optional<unsigned>();
-    }
-};
-
-template class scoped_ext<rel_config>;
-typedef scoped_ext<rel_config> rel_ext;
-
-environment add_relation(environment const & env, name const & n, bool persistent) {
-    return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Relation, n), persistent);
-}
-
-environment add_subst(environment const & env, name const & n, bool persistent) {
-    return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Subst, n), persistent);
-}
-
-environment add_refl(environment const & env, name const & n, bool persistent) {
-    return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Refl, n), persistent);
-}
-
-environment add_symm(environment const & env, name const & n, bool persistent) {
-    return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Symm, n), persistent);
-}
-
-environment add_trans(environment const & env, name const & n, bool persistent) {
-    return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Trans, n), persistent);
-}
-
-static optional<relation_lemma_info> get_info(name_map<relation_lemma_info> const & table, name const & op) {
-    if (auto it = table.find(op)) {
-        return optional<relation_lemma_info>(*it);
-    } else {
-        return optional<relation_lemma_info>();
-    }
-}
-
-optional<refl_info> get_refl_extra_info(environment const & env, name const & op) {
-    return get_info(rel_ext::get_state(env).m_refl_table, op);
-}
-optional<subst_info> get_subst_extra_info(environment const & env, name const & op) {
-    return get_info(rel_ext::get_state(env).m_subst_table, op);
-}
-optional<symm_info> get_symm_extra_info(environment const & env, name const & op) {
-    return get_info(rel_ext::get_state(env).m_symm_table, op);
-}
-
-optional<trans_info> get_trans_extra_info(environment const & env, name const & op1, name const & op2) {
-    if (auto it = rel_ext::get_state(env).m_trans_table.find(mk_pair(op1, op2))) {
-        return optional<trans_info>(*it);
-    } else {
-        return optional<trans_info>();
-    }
-}
-
-bool is_subst_relation(environment const & env, name const & op) {
-    return rel_ext::get_state(env).m_subst_table.contains(op);
-}
-
-optional<name> get_refl_info(environment const & env, name const & op) {
-    if (auto it = get_refl_extra_info(env, op))
-        return optional<name>(it->m_name);
-    else
-        return optional<name>();
-}
-
-optional<name> get_symm_info(environment const & env, name const & op) {
-    if (auto it = get_symm_extra_info(env, op))
-        return optional<name>(it->m_name);
-    else
-        return optional<name>();
-}
-
-optional<name> get_trans_info(environment const & env, name const & op) {
-    if (auto it = get_trans_extra_info(env, op, op))
-        return optional<name>(it->m_name);
-    else
-        return optional<name>();
-}
-
-refl_info_getter mk_refl_info_getter(environment const & env) {
-    auto t = rel_ext::get_state(env).m_refl_table;
-    return [=](name const & n) { return get_info(t, n); }; // NOLINT
-}
-
-trans_info_getter mk_trans_info_getter(environment const & env) {
-    auto t = rel_ext::get_state(env).m_trans_table;
-    return [=](name const & op1, name const & op2) {  // NOLINT
-        if (auto it = t.find(mk_pair(op1, op2))) {
-            return optional<trans_info>(*it);
-        } else {
-            return optional<trans_info>();
-        }
-    };
-}
-
-symm_info_getter mk_symm_info_getter(environment const & env) {
-    auto t = rel_ext::get_state(env).m_symm_table;
-    return [=](name const & n) { return get_info(t, n); }; // NOLINT
-}
-
-bool is_equivalence(environment const & env, name const & rop) {
-    return rel_ext::get_state(env).is_equivalence(rop);
-}
-
-relation_info const * get_relation_info(environment const & env, name const & rop) {
-    return rel_ext::get_state(env).m_rop_table.find(rop);
-}
-
-relation_info_getter mk_relation_info_getter(environment const & env) {
-    auto table = rel_ext::get_state(env).m_rop_table;
-    return [=](name const & rop) { // NOLINT
-        if (auto r = table.find(rop))
-            return optional<relation_info>(*r);
-        else
-            return optional<relation_info>();
-    };
-}
-
-bool is_relation(name_map<relation_info> const & table, expr const & e, name & rop, expr & lhs, expr & rhs) {
-    if (!is_app(e))
-        return false;
-    expr const & f = get_app_fn(e);
-    if (!is_constant(f))
-        return false;
-    auto r = table.find(const_name(f));
-    if (!r)
-        return false;
-    buffer<expr> args;
-    get_app_args(e, args);
-    if (r->get_arity() != args.size())
-        return false;
-    rop = const_name(f);
-    lhs = args[r->get_lhs_pos()];
-    rhs = args[r->get_rhs_pos()];
-    return true;
-}
-
-bool is_relation(environment const & env, expr const & e, name & rop, expr & lhs, expr & rhs) {
-    return is_relation(rel_ext::get_state(env).m_rop_table, e, rop, lhs, rhs);
-}
-
-is_relation_pred mk_is_relation_pred(environment const & env) {
-    name_map<relation_info> table = rel_ext::get_state(env).m_rop_table;
-    return [=](expr const & e, name & rop, expr & lhs, expr & rhs) { // NOLINT
-        return is_relation(table, e, rop, lhs, rhs);
-    };
-}
-
-void initialize_relation_manager() {
-    rel_ext::initialize();
-    register_system_attribute(basic_attribute("refl", "reflexive relation",
-                                              [](environment const & env, io_state const &, name const & d, unsigned,
-                                                 bool persistent) {
-                                                  return add_refl(env, d, persistent);
-                                              }));
-
-    register_system_attribute(basic_attribute("symm", "symmetric relation",
-                                              [](environment const & env, io_state const &, name const & d, unsigned,
-                                                 bool persistent) {
-                                                  return add_symm(env, d, persistent);
-                                              }));
-
-    register_system_attribute(basic_attribute("trans", "transitive relation",
-                                              [](environment const & env, io_state const &, name const & d, unsigned,
-                                                 bool persistent) {
-                                                  return add_trans(env, d, persistent);
-                                              }));
-
-    register_system_attribute(basic_attribute("subst", "substitution",
-                                              [](environment const & env, io_state const &, name const & d, unsigned,
-                                                 bool persistent) {
-                                                  return add_subst(env, d, persistent);
-                                              }));
-}
-
-void finalize_relation_manager() {
-    rel_ext::finalize();
-}
-}
diff --git a/src/library/relation_manager.h b/src/library/relation_manager.h
deleted file mode 100644
index 8965b77c77..0000000000
--- a/src/library/relation_manager.h
+++ /dev/null
@@ -1,98 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/environment.h"
-
-namespace lean {
-struct relation_info {
-    unsigned m_arity;
-    unsigned m_lhs_pos;
-    unsigned m_rhs_pos;
-public:
-    relation_info() {}
-    relation_info(unsigned arity, unsigned lhs, unsigned rhs):
-        m_arity(arity), m_lhs_pos(lhs), m_rhs_pos(rhs) {
-        lean_assert(m_lhs_pos < m_arity);
-        lean_assert(m_rhs_pos < m_arity);
-    }
-    unsigned get_arity() const { return m_arity; }
-    unsigned get_lhs_pos() const { return m_lhs_pos; }
-    unsigned get_rhs_pos() const { return m_rhs_pos; }
-};
-
-/** \brief Return true if \c rop is a registered equivalence relation in the given manager */
-bool is_equivalence(environment const & env, name const & rop);
-
-/** \brief If \c rop is a registered relation, then return a non-null pointer to the associated information
-    Lean assumes that the arguments of the binary relation are the last two explicit arguments.
-    Everything else is assumed to be a parameter.
-*/
-relation_info const * get_relation_info(environment const & env, name const & rop);
-inline bool is_relation(environment const & env, name const & rop) { return get_relation_info(env, rop) != nullptr; }
-
-typedef std::function<optional<relation_info>(name const &)>  relation_info_getter;
-relation_info_getter mk_relation_info_getter(environment const & env);
-
-/** \brief Return true iff \c e is of the form (lhs rop rhs) where rop is a registered relation. */
-bool is_relation(environment const & env, expr const & e, name & rop, expr & lhs, expr & rhs);
-typedef std::function<bool(expr const &, name &, expr &, expr &)> is_relation_pred; // NOLINT
-/** \brief Construct an \c is_relation predicate for the given environment. */
-is_relation_pred mk_is_relation_pred(environment const & env);
-
-/** \brief Declare a new binary relation named \c n */
-environment add_relation(environment const & env, name const & n, bool persistent);
-
-/** \brief Declare subst/refl/symm/trans lemmas for a binary relation,
- * it also declares the relation if it has not been declared yet */
-environment add_subst(environment const & env, name const & n, bool persistent);
-environment add_refl(environment const & env, name const & n, bool persistent);
-environment add_symm(environment const & env, name const & n, bool persistent);
-environment add_trans(environment const & env, name const & n, bool persistent);
-
-struct relation_lemma_info {
-    name     m_name;
-    unsigned m_num_univs;
-    unsigned m_num_args;
-    relation_lemma_info() {}
-    relation_lemma_info(name const & n, unsigned nunivs, unsigned nargs):m_name(n), m_num_univs(nunivs), m_num_args(nargs) {}
-};
-
-typedef relation_lemma_info refl_info;
-typedef relation_lemma_info symm_info;
-typedef relation_lemma_info subst_info;
-
-struct trans_info : public relation_lemma_info {
-    name  m_res_relation;
-    trans_info() {}
-    trans_info(name const & n, unsigned nunivs, unsigned nargs, name const & rel):
-        relation_lemma_info(n, nunivs, nargs), m_res_relation(rel) {}
-};
-
-optional<subst_info> get_subst_extra_info(environment const & env, name const & op);
-optional<refl_info> get_refl_extra_info(environment const & env, name const & op);
-optional<symm_info> get_symm_extra_info(environment const & env, name const & op);
-optional<trans_info> get_trans_extra_info(environment const & env, name const & op1, name const & op2);
-optional<name> get_refl_info(environment const & env, name const & op);
-optional<name> get_symm_info(environment const & env, name const & op);
-optional<name> get_trans_info(environment const & env, name const & op);
-
-typedef std::function<optional<refl_info>(name const &)>  refl_info_getter;
-typedef std::function<optional<trans_info>(name const &, name const &)> trans_info_getter;
-typedef std::function<optional<symm_info>(name const &)>  symm_info_getter;
-
-refl_info_getter mk_refl_info_getter(environment const & env);
-trans_info_getter mk_trans_info_getter(environment const & env);
-symm_info_getter mk_symm_info_getter(environment const & env);
-
-bool is_subst_relation(environment const & env, name const & op);
-inline bool is_trans_relation(environment const & env, name const & op) { return static_cast<bool>(get_trans_info(env, op)); }
-inline bool is_symm_relation(environment const & env, name const & op) { return static_cast<bool>(get_symm_info(env, op)); }
-inline bool is_refl_relation(environment const & env, name const & op) { return static_cast<bool>(get_refl_info(env, op)); }
-
-void initialize_relation_manager();
-void finalize_relation_manager();
-}