diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4ce579f9bf..2b7d0724b7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -331,8 +331,6 @@ add_subdirectory(library)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:library>)
 add_subdirectory(library/tactic)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:tactic>)
-add_subdirectory(library/tactic/defeq_simplifier)
-set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:defeq_simplifier>)
 add_subdirectory(library/tactic/simplifier)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:simplifier>)
 add_subdirectory(library/tactic/backward)
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 37fb45b52e..71afce44b2 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -35,8 +35,6 @@ Author: Leonardo de Moura
 #include "library/compiler/vm_compiler.h"
 #include "library/tactic/kabstract.h"
 #include "library/tactic/elaborate.h"
-#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
-#include "library/tactic/defeq_simplifier/defeq_simplifier.h"
 #include "library/tactic/simplifier/simp_extensions.h"
 #include "library/tactic/tactic_state.h"
 #include "frontends/lean/util.h"
diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp
index b3b4f92b50..6e0bddc2aa 100644
--- a/src/frontends/lean/print_cmd.cpp
+++ b/src/frontends/lean/print_cmd.cpp
@@ -25,8 +25,8 @@ Author: Leonardo de Moura
 #include "library/legacy_type_context.h"
 #include "library/unification_hint.h"
 #include "library/reducible.h"
+#include "library/rfl_lemmas.h"
 #include "library/tactic/kabstract.h"
-#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
 #include "library/tactic/simplifier/simp_lemmas.h"
 #include "library/tactic/simplifier/simp_extensions.h"
 #include "frontends/lean/parser.h"
@@ -475,10 +475,10 @@ static void print_unification_hints(parser & p) {
     out << pp_unification_hints(get_unification_hints(p.env()), out.get_formatter());
 }
 
-static void print_defeq_lemmas(parser & p) {
+static void print_rfl_lemmas(parser & p) {
     type_checker tc(p.env());
     auto out = regular(p.env(), p.ios(), tc);
-    out << pp_defeq_simp_lemmas(*get_defeq_simp_lemmas(p.env()), out.get_formatter());
+    out << pp_rfl_lemmas(*get_rfl_lemmas(p.env()), out.get_formatter());
 }
 
 static void print_simp_rules(parser & p) {
@@ -663,7 +663,7 @@ environment print_cmd(parser & p) {
         else if (name == "unify")
             print_unification_hints(p);
         else if (name == "defeq")
-            print_defeq_lemmas(p);
+            print_rfl_lemmas(p);
         else if (name == "simp")
             print_simp_rules(p);
         else if (name == "simp_ext")
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 2152171036..a328e5165a 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -14,7 +14,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp
   fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp
   mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp
-  aux_definition.cpp inverse.cpp library_system.cpp
+  aux_definition.cpp inverse.cpp library_system.cpp rfl_lemmas.cpp
 
   # Legacy -- The following files will be eventually deleted
   normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp
diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index 4287f6a6ab..51c80a7e63 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -20,7 +20,7 @@ Author: Leonardo de Moura
 #include "library/aux_definition.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/compiler/vm_compiler.h"
-#include "library/tactic/defeq_simplifier/defeq_simplifier.h"
+#include "library/tactic/defeq_simplifier.h"
 #include "library/equations_compiler/equations.h"
 #include "library/equations_compiler/util.h"
 
@@ -301,7 +301,7 @@ static environment add_equation_lemma(environment const & env, options const & o
     if (use_dsimp) {
         try {
             type_context ctx(env, opts, mctx, lctx, transparency_mode::None);
-            defeq_simp_lemmas_ptr lemmas = get_defeq_simp_lemmas(env, g_eqn_sanitizer_token);
+            rfl_lemmas_ptr lemmas = get_rfl_lemmas(env, g_eqn_sanitizer_token);
             new_type = defeq_simplify(ctx, *lemmas, type);
         } catch (defeq_simplifier_exception & ex) {
             throw nested_exception("equation compiler failed to simplify type of automatically generated lemma using "
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 1089ed580e..0e284153bb 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -48,6 +48,7 @@ Author: Leonardo de Moura
 #include "library/mpq_macro.h"
 #include "library/arith_instance_manager.h"
 #include "library/inverse.h"
+#include "library/rfl_lemmas.h"
 
 // #include "library/congr_lemma_manager.h"
 // #include "library/light_lt_manager.h"
@@ -122,6 +123,7 @@ void initialize_library_module() {
     // initialize_congr_lemma_manager();
     initialize_fun_info();
     initialize_unification_hint();
+    initialize_rfl_lemmas();
     initialize_type_context();
     initialize_delayed_abstraction();
     initialize_mpq_macro();
@@ -135,6 +137,7 @@ void finalize_library_module() {
     finalize_mpq_macro();
     finalize_delayed_abstraction();
     finalize_type_context();
+    finalize_rfl_lemmas();
     finalize_unification_hint();
     finalize_fun_info();
     // finalize_congr_lemma_manager();
diff --git a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp b/src/library/rfl_lemmas.cpp
similarity index 56%
rename from src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp
rename to src/library/rfl_lemmas.cpp
index 4667581426..b07d82f40c 100644
--- a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp
+++ b/src/library/rfl_lemmas.cpp
@@ -15,26 +15,26 @@ Author: Daniel Selsam, Leonardo de Moura
 #include "library/util.h"
 #include "library/scoped_ext.h"
 #include "library/type_context.h"
-#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
+#include "library/rfl_lemmas.h"
 
 namespace lean {
-defeq_simp_lemma::defeq_simp_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
-                                   list<bool> const & instances, expr const & lhs, expr const & rhs, unsigned priority):
+rfl_lemma::rfl_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
+                     list<bool> const & instances, expr const & lhs, expr const & rhs, unsigned priority):
     m_id(id), m_umetas(umetas), m_emetas(emetas), m_instances(instances), m_lhs(lhs), m_rhs(rhs), m_priority(priority) {}
 
-bool operator==(defeq_simp_lemma const & sl1, defeq_simp_lemma const & sl2) {
+bool operator==(rfl_lemma const & sl1, rfl_lemma const & sl2) {
     return sl1.get_lhs() == sl2.get_lhs() && sl1.get_rhs() == sl2.get_rhs();
 }
 
 static void throw_non_rfl_proof() {
-    throw exception("invalid [defeq] simp lemma: proof must be an application of either 'eq.refl' or 'rfl'");
+    throw exception("invalid reflexivity lemma: proof must be an application of either 'eq.refl' or 'rfl'");
 }
 
-static void on_add_defeq_simp_lemma(environment const & env, name const & decl_name, bool) {
+static void on_add_rfl_lemma(environment const & env, name const & decl_name, bool) {
     type_context ctx(env);
     declaration const & d = env.get(decl_name);
     if (!d.is_definition()) {
-        throw exception("invalid [defeq] simp lemma: must be a definition so that definitional equality can be verified");
+        throw exception("invalid reflexivity lemma: must be a definition so that definitional equality can be verified");
     }
     expr type = d.get_type();
     expr pf   = d.get_value();
@@ -46,15 +46,15 @@ static void on_add_defeq_simp_lemma(environment const & env, name const & decl_n
     }
     expr lhs, rhs;
     if (!is_eq(type, lhs, rhs))
-        throw exception("invalid [defeq] simp lemma: body must be an equality");
+        throw exception("invalid reflexivity lemma: body must be an equality");
     if (!is_app_of(pf, get_eq_refl_name(), 2) && !is_app_of(pf, get_rfl_name(), 2))
         throw_non_rfl_proof();
     if (lhs == rhs)
-        throw exception("invalid [defeq] simp lemma: the two sides of the equality cannot be structurally equal");
+        throw exception("invalid reflexivity lemma: the two sides of the equality cannot be structurally equal");
 }
 
 static void add_lemma_core(tmp_type_context & ctx, name const & decl_name, unsigned priority,
-                           defeq_simp_lemmas_ptr & result) {
+                           rfl_lemmas_ptr & result) {
     environment const & env = ctx.env();
     declaration const & d   = env.get(decl_name);
     lean_assert(d.is_definition());
@@ -75,16 +75,16 @@ static void add_lemma_core(tmp_type_context & ctx, name const & decl_name, unsig
     }
     expr lhs, rhs;
     lean_verify(is_eq(type, lhs, rhs));
-    defeq_simp_lemma lemma(decl_name, to_list(umetas), to_list(emetas), to_list(instances), lhs, rhs, priority);
+    rfl_lemma lemma(decl_name, to_list(umetas), to_list(emetas), to_list(instances), lhs, rhs, priority);
     result->insert(lhs, lemma);
 }
 
-static defeq_simp_lemmas_ptr get_defeq_simp_lemmas_from_attribute(type_context & ctx, name const & attr_name) {
+static rfl_lemmas_ptr get_rfl_lemmas_from_attribute(type_context & ctx, name const & attr_name) {
     environment const & env = ctx.env();
     auto const & attr       = get_attribute(env, attr_name);
     buffer<name> lemmas;
     attr.get_instances(env, lemmas);
-    defeq_simp_lemmas_ptr result = std::make_shared<defeq_simp_lemmas>();
+    rfl_lemmas_ptr result = std::make_shared<rfl_lemmas>();
     unsigned i = lemmas.size();
     while (i > 0) {
         i--;
@@ -96,28 +96,28 @@ static defeq_simp_lemmas_ptr get_defeq_simp_lemmas_from_attribute(type_context &
     return result;
 }
 
-static defeq_simp_lemmas_ptr get_defeq_simp_lemmas_from_attribute(environment const & env, name const & attr_name) {
+static rfl_lemmas_ptr get_rfl_lemmas_from_attribute(environment const & env, name const & attr_name) {
     type_context ctx(env);
-    return get_defeq_simp_lemmas_from_attribute(ctx, attr_name);
+    return get_rfl_lemmas_from_attribute(ctx, attr_name);
 }
 
-static std::vector<name> * g_defeq_simp_attributes = nullptr;
-static defeq_lemmas_token  g_default_token;
+static std::vector<name> * g_rfl_lemmas_attributes = nullptr;
+static rfl_lemmas_token    g_default_token;
 
-defeq_lemmas_token register_defeq_simp_attribute(name const & attr_name) {
-    unsigned r = g_defeq_simp_attributes->size();
-    g_defeq_simp_attributes->push_back(attr_name);
-    register_system_attribute(basic_attribute::with_check(attr_name, "[defeq] simplification lemma",
-                                                          on_add_defeq_simp_lemma));
+rfl_lemmas_token register_defeq_simp_attribute(name const & attr_name) {
+    unsigned r = g_rfl_lemmas_attributes->size();
+    g_rfl_lemmas_attributes->push_back(attr_name);
+    register_system_attribute(basic_attribute::with_check(attr_name, "reflexivity lemma",
+                                                          on_add_rfl_lemma));
     return r;
 }
 
-class defeq_simp_lemmas_cache {
+class rfl_lemmas_cache {
     struct entry {
-        environment           m_env;
-        name                  m_attr_name;
-        unsigned              m_attr_fingerprint;
-        defeq_simp_lemmas_ptr m_lemmas;
+        environment    m_env;
+        name           m_attr_name;
+        unsigned       m_attr_fingerprint;
+        rfl_lemmas_ptr m_lemmas;
         entry(environment const & env, name const & attr_name):
             m_env(env), m_attr_name(attr_name), m_attr_fingerprint(0) {}
     };
@@ -125,25 +125,25 @@ class defeq_simp_lemmas_cache {
 public:
     void expand(environment const & env, unsigned new_sz) {
         for (unsigned i = m_entries.size(); i < new_sz; i++) {
-            m_entries.emplace_back(env, (*g_defeq_simp_attributes)[i]);
+            m_entries.emplace_back(env, (*g_rfl_lemmas_attributes)[i]);
         }
     }
 
-    defeq_simp_lemmas_ptr mk_lemmas(environment const & env, entry & C) {
-        lean_trace("defeq_simp_lemmas_cache", tout() << "make defeq simp lemmas [" << C.m_attr_name << "]\n";);
+    rfl_lemmas_ptr mk_lemmas(environment const & env, entry & C) {
+        lean_trace("rfl_lemmas_cache", tout() << "make reflexivity lemmas [" << C.m_attr_name << "]\n";);
         C.m_env              = env;
-        C.m_lemmas           = get_defeq_simp_lemmas_from_attribute(env, C.m_attr_name);
+        C.m_lemmas           = get_rfl_lemmas_from_attribute(env, C.m_attr_name);
         C.m_attr_fingerprint = get_attribute_fingerprint(env, C.m_attr_name);
         return C.m_lemmas;
     }
 
-    defeq_simp_lemmas_ptr lemmas_of(entry const & C) {
-        lean_trace("defeq_simp_lemmas_cache", tout() << "reusing cached defeq simp lemmas [" << C.m_attr_name << "]\n";);
+    rfl_lemmas_ptr lemmas_of(entry const & C) {
+        lean_trace("rfl_lemmas_cache", tout() << "reusing cached reflexivity lemmas [" << C.m_attr_name << "]\n";);
         return C.m_lemmas;
     }
 
-    defeq_simp_lemmas_ptr get(environment const & env, defeq_lemmas_token token) {
-        lean_assert(token < g_defeq_simp_attributes->size());
+    rfl_lemmas_ptr get(environment const & env, rfl_lemmas_token token) {
+        lean_assert(token < g_rfl_lemmas_attributes->size());
         if (token >= m_entries.size()) expand(env, token+1);
         lean_assert(token < m_entries.size());
         entry & C = m_entries[token];
@@ -151,7 +151,7 @@ public:
         if (is_eqp(env, C.m_env)) return lemmas_of(C);
         if (!env.is_descendant(C.m_env) ||
             get_attribute_fingerprint(env, C.m_attr_name) != C.m_attr_fingerprint) {
-            lean_trace("defeq_simp_lemmas_cache",
+            lean_trace("rfl_lemmas_cache",
                        bool c = (get_attribute_fingerprint(env, C.m_attr_name) == C.m_attr_fingerprint);
                        tout() << "creating new cache, is_descendant: " << env.is_descendant(C.m_env)
                        << ", attribute fingerprint compatibility: " << c << "\n";);
@@ -161,43 +161,43 @@ public:
     }
 };
 
-MK_THREAD_LOCAL_GET_DEF(defeq_simp_lemmas_cache, get_cache);
+MK_THREAD_LOCAL_GET_DEF(rfl_lemmas_cache, get_cache);
 
-defeq_simp_lemmas_ptr get_defeq_simp_lemmas(environment const & env) {
+rfl_lemmas_ptr get_rfl_lemmas(environment const & env) {
     return get_cache().get(env, g_default_token);
 }
 
-defeq_simp_lemmas_ptr get_defeq_simp_lemmas(environment const & env, defeq_lemmas_token token) {
+rfl_lemmas_ptr get_rfl_lemmas(environment const & env, rfl_lemmas_token token) {
     return get_cache().get(env, token);
 }
 
-format defeq_simp_lemma::pp(formatter const & fmt) const {
+format rfl_lemma::pp(formatter const & fmt) const {
     format r;
-    r += format("#") + format(get_num_emeta());
+    r += format(m_id) + space() + format("#") + format(get_num_emeta());
     if (get_priority() != LEAN_DEFAULT_PRIORITY)
-        r += space() + paren(format(get_priority()));
+        r += space() + paren(format("prio:") + space() + format(get_priority()));
     format r1 = comma() + space() + fmt(get_lhs());
     r1       += space() + format("↦") + pp_indent_expr(fmt, get_rhs());
     r += group(r1);
     return r;
 }
 
-format pp_defeq_simp_lemmas(defeq_simp_lemmas const & lemmas, formatter const & fmt) {
+format pp_rfl_lemmas(rfl_lemmas const & lemmas, formatter const & fmt) {
     format r;
-    r += format("defeq simp lemmas") + colon() + line();
-    lemmas.for_each_entry([&](head_index const &, defeq_simp_lemma const & lemma) {
+    r += format("reflexivity lemmas") + colon() + line();
+    lemmas.for_each_entry([&](head_index const &, rfl_lemma const & lemma) {
              r += lemma.pp(fmt) + line();
         });
     return r;
 }
 
-void initialize_defeq_simp_lemmas() {
-    register_trace_class("defeq_simp_lemmas_cache");
-    g_defeq_simp_attributes = new std::vector<name>();
+void initialize_rfl_lemmas() {
+    register_trace_class("rfl_lemmas_cache");
+    g_rfl_lemmas_attributes = new std::vector<name>();
     g_default_token         = register_defeq_simp_attribute("defeq");
 }
 
-void finalize_defeq_simp_lemmas() {
-    delete g_defeq_simp_attributes;
+void finalize_rfl_lemmas() {
+    delete g_rfl_lemmas_attributes;
 }
 }
diff --git a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.h b/src/library/rfl_lemmas.h
similarity index 55%
rename from src/library/tactic/defeq_simplifier/defeq_simp_lemmas.h
rename to src/library/rfl_lemmas.h
index 7b53cc8eac..b2b05527d4 100644
--- a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.h
+++ b/src/library/rfl_lemmas.h
@@ -9,8 +9,7 @@ Author: Daniel Selsam
 #include "library/head_map.h"
 
 namespace lean {
-
-class defeq_simp_lemma {
+class rfl_lemma {
     name                m_id;
     levels              m_umetas;
     list<expr>          m_emetas;
@@ -20,9 +19,9 @@ class defeq_simp_lemma {
     expr                m_rhs;
     unsigned            m_priority;
 public:
-    defeq_simp_lemma() {}
-    defeq_simp_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
-                     list<bool> const & instances, expr const & lhs, expr const & rhs, unsigned priority);
+    rfl_lemma() {}
+    rfl_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
+              list<bool> const & instances, expr const & lhs, expr const & rhs, unsigned priority);
 
     name const & get_id() const { return m_id; }
     unsigned get_num_umeta() const { return length(m_umetas); }
@@ -42,24 +41,24 @@ public:
     format pp(formatter const & fmt) const;
 };
 
-bool operator==(defeq_simp_lemma const & sl1, defeq_simp_lemma const & sl2);
-inline bool operator!=(defeq_simp_lemma const & sl1, defeq_simp_lemma const & sl2) { return !operator==(sl1, sl2); }
+bool operator==(rfl_lemma const & sl1, rfl_lemma const & sl2);
+inline bool operator!=(rfl_lemma const & sl1, rfl_lemma const & sl2) { return !operator==(sl1, sl2); }
 
-struct defeq_simp_lemma_prio_fn { unsigned operator()(defeq_simp_lemma const & sl) const { return sl.get_priority(); } };
-typedef head_map_prio<defeq_simp_lemma, defeq_simp_lemma_prio_fn> defeq_simp_lemmas;
+struct rfl_lemma_prio_fn { unsigned operator()(rfl_lemma const & sl) const { return sl.get_priority(); } };
+typedef head_map_prio<rfl_lemma, rfl_lemma_prio_fn> rfl_lemmas;
 
-typedef unsigned defeq_lemmas_token;
+typedef unsigned rfl_lemmas_token;
 
 /* Register a system level defeq attribute. This method must only be invoked during initialization.
    It returns an internal "token" for retrieving the lemmas */
-defeq_lemmas_token register_defeq_simp_attribute(name const & attr_name);
+rfl_lemmas_token register_defeq_simp_attribute(name const & attr_name);
 
-typedef std::shared_ptr<defeq_simp_lemmas> defeq_simp_lemmas_ptr;
-defeq_simp_lemmas_ptr get_defeq_simp_lemmas(environment const & env);
-defeq_simp_lemmas_ptr get_defeq_simp_lemmas(environment const & env, defeq_lemmas_token token);
+typedef std::shared_ptr<rfl_lemmas> rfl_lemmas_ptr;
+rfl_lemmas_ptr get_rfl_lemmas(environment const & env);
+rfl_lemmas_ptr get_rfl_lemmas(environment const & env, rfl_lemmas_token token);
 
-format pp_defeq_simp_lemmas(defeq_simp_lemmas const & lemmas, formatter const & fmt);
+format pp_rfl_lemmas(rfl_lemmas const & lemmas, formatter const & fmt);
 
-void initialize_defeq_simp_lemmas();
-void finalize_defeq_simp_lemmas();
+void initialize_rfl_lemmas();
+void finalize_rfl_lemmas();
 }
diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index f7bae22c27..0e3e6060fa 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -6,4 +6,4 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp
   ac_tactics.cpp induction_tactic.cpp cases_tactic.cpp
   generalize_tactic.cpp rewrite_tactic.cpp unfold_tactic.cpp
   hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp
-  simp_result.cpp user_attribute.cpp)
+  simp_result.cpp user_attribute.cpp defeq_simplifier.cpp)
diff --git a/src/library/tactic/defeq_simplifier/defeq_simplifier.cpp b/src/library/tactic/defeq_simplifier.cpp
similarity index 95%
rename from src/library/tactic/defeq_simplifier/defeq_simplifier.cpp
rename to src/library/tactic/defeq_simplifier.cpp
index 29cb82febb..434a5eb847 100644
--- a/src/library/tactic/defeq_simplifier/defeq_simplifier.cpp
+++ b/src/library/tactic/defeq_simplifier.cpp
@@ -15,7 +15,7 @@ Author: Daniel Selsam
 #include "library/defeq_canonizer.h"
 #include "library/vm/vm_expr.h"
 #include "library/tactic/tactic_state.h"
-#include "library/tactic/defeq_simplifier/defeq_simplifier.h"
+#include "library/tactic/defeq_simplifier.h"
 
 #ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS
 #define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS 5000
@@ -75,7 +75,7 @@ static bool get_simplify_canonize_proofs(options const & o) {
 class defeq_simplify_fn {
     type_context           & m_ctx;
 
-    defeq_simp_lemmas        m_simp_lemmas;
+    rfl_lemmas               m_simp_lemmas;
 
     unsigned                 m_num_simp_rounds{0};
     unsigned                 m_num_rewrite_rounds{0};
@@ -246,19 +246,19 @@ class defeq_simplify_fn {
                                                  "the current limit is " << m_max_rewrite_rounds << ") "
                                                  "(use `set_option trace.defeq_simplifier true` to obtain more information");
             }
-            list<defeq_simp_lemma> const * simp_lemmas_ptr = m_simp_lemmas.find(e);
+            list<rfl_lemma> const * simp_lemmas_ptr = m_simp_lemmas.find(e);
             if (!simp_lemmas_ptr) return e;
-            buffer<defeq_simp_lemma> simp_lemmas;
+            buffer<rfl_lemma> simp_lemmas;
             to_buffer(*simp_lemmas_ptr, simp_lemmas);
 
             expr e_start = e;
-            for (defeq_simp_lemma const & sl : simp_lemmas) e = rewrite(e, sl);
+            for (rfl_lemma const & sl : simp_lemmas) e = rewrite(e, sl);
             if (e == e_start) break;
         }
         return e;
     }
 
-    expr rewrite(expr const & e, defeq_simp_lemma const & sl) {
+    expr rewrite(expr const & e, rfl_lemma const & sl) {
         type_context::tmp_mode_scope scope(m_ctx, sl.get_num_umeta(), sl.get_num_emeta());
         if (!m_ctx.is_def_eq(e, sl.get_lhs())) return e;
 
@@ -320,7 +320,7 @@ class defeq_simplify_fn {
     }
 
 public:
-    defeq_simplify_fn(type_context & ctx, defeq_simp_lemmas const & simp_lemmas):
+    defeq_simplify_fn(type_context & ctx, rfl_lemmas const & simp_lemmas):
         m_ctx(ctx),
         m_simp_lemmas(simp_lemmas),
         m_max_simp_rounds(get_simplify_max_simp_rounds(ctx.get_options())),
@@ -346,7 +346,7 @@ public:
 };
 
 /* Entry point */
-expr defeq_simplify(type_context & ctx, defeq_simp_lemmas const & simp_lemmas, expr const & e) {
+expr defeq_simplify(type_context & ctx, rfl_lemmas const & simp_lemmas, expr const & e) {
     return defeq_simplify_fn(ctx, simp_lemmas)(e);
 }
 
@@ -354,14 +354,14 @@ vm_obj tactic_defeq_simp(vm_obj const & m, vm_obj const & e, vm_obj const & s0)
     type_context ctx = mk_type_context_for(s0, m);
     tactic_state const & s    = to_tactic_state(s0);
     LEAN_TACTIC_TRY;
-    defeq_simp_lemmas_ptr lemmas = get_defeq_simp_lemmas(s.env());
+    rfl_lemmas_ptr lemmas = get_rfl_lemmas(s.env());
     expr new_e                   = defeq_simplify(ctx, *lemmas, to_expr(e));
     return mk_tactic_success(to_obj(new_e), s);
     LEAN_TACTIC_CATCH(s);
 }
 
 expr defeq_simplify(type_context & ctx, expr const & e) {
-    defeq_simp_lemmas_ptr lemmas  = get_defeq_simp_lemmas(ctx.env());
+    rfl_lemmas_ptr lemmas  = get_rfl_lemmas(ctx.env());
     return defeq_simplify(ctx, *lemmas, e);
 }
 
diff --git a/src/library/tactic/defeq_simplifier/defeq_simplifier.h b/src/library/tactic/defeq_simplifier.h
similarity index 82%
rename from src/library/tactic/defeq_simplifier/defeq_simplifier.h
rename to src/library/tactic/defeq_simplifier.h
index bceceb32ea..1dff671a78 100644
--- a/src/library/tactic/defeq_simplifier/defeq_simplifier.h
+++ b/src/library/tactic/defeq_simplifier.h
@@ -6,7 +6,7 @@ Author: Daniel Selsam
 #pragma once
 #include "kernel/expr.h"
 #include "library/type_context.h"
-#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
+#include "library/rfl_lemmas.h"
 
 namespace lean {
 class defeq_simplifier_exception : public exception {
@@ -17,7 +17,7 @@ public:
     virtual void rethrow() const override { throw *this; }
 };
 
-expr defeq_simplify(type_context & ctx, defeq_simp_lemmas const & simp_lemmas, expr const & e);
+expr defeq_simplify(type_context & ctx, rfl_lemmas const & simp_lemmas, expr const & e);
 expr defeq_simplify(type_context & ctx, expr const & e);
 void initialize_defeq_simplifier();
 void finalize_defeq_simplifier();
diff --git a/src/library/tactic/defeq_simplifier/CMakeLists.txt b/src/library/tactic/defeq_simplifier/CMakeLists.txt
deleted file mode 100644
index 7c76de2705..0000000000
--- a/src/library/tactic/defeq_simplifier/CMakeLists.txt
+++ /dev/null
@@ -1 +0,0 @@
-add_library(defeq_simplifier OBJECT init_module.cpp defeq_simp_lemmas.cpp defeq_simplifier.cpp)
diff --git a/src/library/tactic/defeq_simplifier/init_module.cpp b/src/library/tactic/defeq_simplifier/init_module.cpp
deleted file mode 100644
index 3612850e7a..0000000000
--- a/src/library/tactic/defeq_simplifier/init_module.cpp
+++ /dev/null
@@ -1,20 +0,0 @@
-/*
-Copyright (c) 2016 Daniel Selsam. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Daniel Selsam
-*/
-#include "library/tactic/defeq_simplifier/defeq_simplifier.h"
-#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
-
-namespace lean {
-
-void initialize_defeq_simplifier_module() {
-    initialize_defeq_simp_lemmas();
-    initialize_defeq_simplifier();
-}
-
-void finalize_defeq_simplifier_module() {
-    finalize_defeq_simplifier();
-    finalize_defeq_simp_lemmas();
-}
-}
diff --git a/src/library/tactic/defeq_simplifier/init_module.h b/src/library/tactic/defeq_simplifier/init_module.h
deleted file mode 100644
index 7782095b7d..0000000000
--- a/src/library/tactic/defeq_simplifier/init_module.h
+++ /dev/null
@@ -1,11 +0,0 @@
-/*
-Copyright (c) 2016 Daniel Selsam. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Daniel Selsam
-*/
-#pragma once
-
-namespace lean {
-void initialize_defeq_simplifier_module();
-void finalize_defeq_simplifier_module();
-}
diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp
index d196dbb5f5..1119616878 100644
--- a/src/library/tactic/init_module.cpp
+++ b/src/library/tactic/init_module.cpp
@@ -27,7 +27,7 @@ Author: Leonardo de Moura
 #include "library/tactic/unfold_tactic.h"
 #include "library/tactic/elaborate.h"
 #include "library/tactic/user_attribute.h"
-#include "library/tactic/defeq_simplifier/init_module.h"
+#include "library/tactic/defeq_simplifier.h"
 #include "library/tactic/simplifier/init_module.h"
 #include "library/tactic/backward/init_module.h"
 
@@ -54,7 +54,7 @@ void initialize_tactic_module() {
     initialize_generalize_tactic();
     initialize_rewrite_tactic();
     initialize_unfold_tactic();
-    initialize_defeq_simplifier_module();
+    initialize_defeq_simplifier();
     initialize_simplifier_module();
     initialize_backward_module();
     initialize_elaborate();
@@ -65,7 +65,7 @@ void finalize_tactic_module() {
     finalize_elaborate();
     finalize_backward_module();
     finalize_simplifier_module();
-    finalize_defeq_simplifier_module();
+    finalize_defeq_simplifier();
     finalize_unfold_tactic();
     finalize_rewrite_tactic();
     finalize_generalize_tactic();
diff --git a/tests/lean/defeq_simp_lemmas1.lean.expected.out b/tests/lean/defeq_simp_lemmas1.lean.expected.out
index 54e620ad99..92eaf77419 100644
--- a/tests/lean/defeq_simp_lemmas1.lean.expected.out
+++ b/tests/lean/defeq_simp_lemmas1.lean.expected.out
@@ -1,22 +1,22 @@
-defeq simp lemmas:
-#4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
-#3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
-#4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
-#2, sizeof list.nil ↦ 1
-#3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
-#2, sizeof none ↦ 1
-#1, sizeof ?x_0 ↦ nat.of_num ?x_0
-#1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
-#1, sizeof ?x_0 ↦ 1
-#1, sizeof ?x_0 ↦ 1
-#1, sizeof ?x_0 ↦ 1
-#6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
-#5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
-#5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
-#6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
-#1, sizeof ?x_0 ↦ ?x_0
-#2, sizeof ?x_1 ↦ 0
-#2, id ?x_1 ↦ ?x_1
-#2, g ?x_0 ?x_1 ↦ h ?x_1
-#3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
-#1, h ?x_0 ↦ q ?x_0
+reflexivity lemmas:
+foo.d.def #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
+foo.f.def #3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
+sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
+sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
+sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
+sizeof_option_none_eq #2, sizeof none ↦ 1
+sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
+sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
+sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
+sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
+sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
+sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
+sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
+sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
+sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
+sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
+default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
+id.def #2, id ?x_1 ↦ ?x_1
+foo.g.def #2, g ?x_0 ?x_1 ↦ h ?x_1
+ne.def #3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
+foo.h.def #1, h ?x_0 ↦ q ?x_0
diff --git a/tests/lean/defeq_simp_lemmas2.lean.expected.out b/tests/lean/defeq_simp_lemmas2.lean.expected.out
index d1b0f78920..935d9cc409 100644
--- a/tests/lean/defeq_simp_lemmas2.lean.expected.out
+++ b/tests/lean/defeq_simp_lemmas2.lean.expected.out
@@ -1,78 +1,78 @@
-defeq simp lemmas:
-#4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
-#4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
-#3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
-#3, f ?x_0 ?x_1 ?x_2 ↦ ?x_2
-#4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
-#2, sizeof list.nil ↦ 1
-#3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
-#2, sizeof none ↦ 1
-#1, sizeof ?x_0 ↦ nat.of_num ?x_0
-#1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
-#1, sizeof ?x_0 ↦ 1
-#1, sizeof ?x_0 ↦ 1
-#1, sizeof ?x_0 ↦ 1
-#6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
-#5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
-#5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
-#6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
-#1, sizeof ?x_0 ↦ ?x_0
-#2, sizeof ?x_1 ↦ 0
-#2, id ?x_1 ↦ ?x_1
-#2, g ?x_0 ?x_1 ↦ h ?x_1
-#2, g ?x_0 ?x_1 ↦ ?x_1
-#3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
-#1, h ?x_0 ↦ q ?x_0
-#1, h ?x_0 ↦ ?x_0
-defeq simp lemmas:
-#4 (1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
-#4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
-#3 (1001), f ?x_0 ?x_1 ?x_2 ↦ ?x_2
-#3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
-#4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
-#2, sizeof list.nil ↦ 1
-#3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
-#2, sizeof none ↦ 1
-#1, sizeof ?x_0 ↦ nat.of_num ?x_0
-#1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
-#1, sizeof ?x_0 ↦ 1
-#1, sizeof ?x_0 ↦ 1
-#1, sizeof ?x_0 ↦ 1
-#6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
-#5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
-#5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
-#6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
-#1, sizeof ?x_0 ↦ ?x_0
-#2, sizeof ?x_1 ↦ 0
-#2, id ?x_1 ↦ ?x_1
-#2 (1001), g ?x_0 ?x_1 ↦ ?x_1
-#2, g ?x_0 ?x_1 ↦ h ?x_1
-#3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
-#1 (1001), h ?x_0 ↦ ?x_0
-#1, h ?x_0 ↦ q ?x_0
-defeq simp lemmas:
-#4 (1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
-#4 (1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
-#3 (1001), f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
-#3 (1001), f ?x_0 ?x_1 ?x_2 ↦ ?x_2
-#4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
-#2, sizeof list.nil ↦ 1
-#3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
-#2, sizeof none ↦ 1
-#1, sizeof ?x_0 ↦ nat.of_num ?x_0
-#1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
-#1, sizeof ?x_0 ↦ 1
-#1, sizeof ?x_0 ↦ 1
-#1, sizeof ?x_0 ↦ 1
-#6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
-#5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
-#5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
-#6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
-#1, sizeof ?x_0 ↦ ?x_0
-#2, sizeof ?x_1 ↦ 0
-#2, id ?x_1 ↦ ?x_1
-#2 (1001), g ?x_0 ?x_1 ↦ h ?x_1
-#2 (1001), g ?x_0 ?x_1 ↦ ?x_1
-#3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
-#1 (1001), h ?x_0 ↦ q ?x_0
-#1 (1001), h ?x_0 ↦ ?x_0
+reflexivity lemmas:
+foo.d.def #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
+foo.d.rfl #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
+foo.f.def #3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
+foo.f.rfl #3, f ?x_0 ?x_1 ?x_2 ↦ ?x_2
+sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
+sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
+sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
+sizeof_option_none_eq #2, sizeof none ↦ 1
+sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
+sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
+sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
+sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
+sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
+sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
+sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
+sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
+sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
+sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
+default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
+id.def #2, id ?x_1 ↦ ?x_1
+foo.g.def #2, g ?x_0 ?x_1 ↦ h ?x_1
+foo.g.rfl #2, g ?x_0 ?x_1 ↦ ?x_1
+ne.def #3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
+foo.h.def #1, h ?x_0 ↦ q ?x_0
+foo.h.rfl #1, h ?x_0 ↦ ?x_0
+reflexivity lemmas:
+foo.d.rfl #4 (prio: 1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
+foo.d.def #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
+foo.f.rfl #3 (prio: 1001), f ?x_0 ?x_1 ?x_2 ↦ ?x_2
+foo.f.def #3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
+sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
+sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
+sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
+sizeof_option_none_eq #2, sizeof none ↦ 1
+sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
+sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
+sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
+sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
+sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
+sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
+sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
+sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
+sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
+sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
+default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
+id.def #2, id ?x_1 ↦ ?x_1
+foo.g.rfl #2 (prio: 1001), g ?x_0 ?x_1 ↦ ?x_1
+foo.g.def #2, g ?x_0 ?x_1 ↦ h ?x_1
+ne.def #3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
+foo.h.rfl #1 (prio: 1001), h ?x_0 ↦ ?x_0
+foo.h.def #1, h ?x_0 ↦ q ?x_0
+reflexivity lemmas:
+foo.d.def #4 (prio: 1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
+foo.d.rfl #4 (prio: 1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
+foo.f.def #3 (prio: 1001), f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
+foo.f.rfl #3 (prio: 1001), f ?x_0 ?x_1 ?x_2 ↦ ?x_2
+sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
+sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
+sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
+sizeof_option_none_eq #2, sizeof none ↦ 1
+sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
+sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
+sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
+sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
+sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
+sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
+sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
+sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
+sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
+sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
+default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
+id.def #2, id ?x_1 ↦ ?x_1
+foo.g.def #2 (prio: 1001), g ?x_0 ?x_1 ↦ h ?x_1
+foo.g.rfl #2 (prio: 1001), g ?x_0 ?x_1 ↦ ?x_1
+ne.def #3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
+foo.h.def #1 (prio: 1001), h ?x_0 ↦ q ?x_0
+foo.h.rfl #1 (prio: 1001), h ?x_0 ↦ ?x_0