diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 623305a9e..6c04dc024 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -57,7 +57,7 @@
            "whnf" "multiple_instances" "none" "decl" "declaration"
            "relation" "symm" "subst" "refl" "trans" "simp" "congr"
            "backward" "forward" "no_pattern" "begin_end" "tactic" "abbreviation"
-           "reducible" "unfold" "alias" "eqv" "intro" "intro!" "elim" "grinder" "unify"
+           "reducible" "unfold" "alias" "eqv" "intro" "intro!" "elim" "grinder" "unify" "defeq"
            "localrefinfo" "recursor"))
   "lean modifiers")
 (defconst lean-modifiers-regexp
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 6168f7826..801834c0e 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -25,6 +25,8 @@ Author: Leonardo de Moura
 #include "library/fun_info_manager.h"
 #include "library/congr_lemma_manager.h"
 #include "library/abstract_expr_manager.h"
+#include "library/defeq_simp_lemmas.h"
+#include "library/defeq_simplifier.h"
 #include "library/definitional/projection.h"
 #include "library/blast/blast.h"
 #include "library/blast/simplifier/simplifier.h"
@@ -796,6 +798,38 @@ static environment unify_cmd(parser & p) {
     return env;
 }
 
+static environment defeq_simplify_cmd(parser & p) {
+    auto pos = p.pos();
+    environment const & env = p.env();
+    name ns = p.check_id_next("invalid #simplify command, namespace or 'env' expected");
+
+    defeq_simp_lemmas sls;
+    if (ns == name("null")) {
+    } else if (ns == name("env")) {
+        sls = get_defeq_simp_lemmas(env);
+    } else {
+        sls = get_defeq_simp_lemmas(env, ns);
+    }
+
+    expr e; level_param_names ls;
+    std::tie(e, ls) = parse_local_expr(p);
+
+    auto tc = mk_type_checker(p.env());
+
+    expr e_simp = defeq_simplify(env, p.get_options(), sls, e);
+    if (!tc->is_def_eq(e, e_simp).first) {
+        throw parser_error("defeq_simplify result not definitionally equal to input expression", pos);
+    }
+    flycheck_information info(p.regular_stream());
+    if (info.enabled()) {
+        p.display_information_pos(p.cmd_pos());
+        p.regular_stream() << "defeq_simplify result:\n";
+    }
+
+    p.regular_stream() << e_simp << endl;
+    return env;
+}
+
 static environment abstract_expr_cmd(parser & p) {
     unsigned o = p.parse_small_nat();
     default_type_context ctx(p.env(), p.get_options());
@@ -861,6 +895,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#unify",            "(for debugging purposes)", unify_cmd));
     add_cmd(r, cmd_info("#accessible",       "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd));
     add_cmd(r, cmd_info("#simplify",         "(for debugging purposes) simplify given expression", simplify_cmd));
+    add_cmd(r, cmd_info("#defeq_simplify",   "(for debugging purposes) defeq-simplify given expression", defeq_simplify_cmd));
     add_cmd(r, cmd_info("#abstract_expr",    "(for debugging purposes) call abstract expr methods", abstract_expr_cmd));
 
     register_decl_cmds(r);
diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp
index dc9433bdd..1c9563c6e 100644
--- a/src/frontends/lean/print_cmd.cpp
+++ b/src/frontends/lean/print_cmd.cpp
@@ -27,6 +27,7 @@ Author: Leonardo de Moura
 #include "library/relation_manager.h"
 #include "library/noncomputable.h"
 #include "library/unification_hint.h"
+#include "library/defeq_simp_lemmas.h"
 #include "library/definitional/projection.h"
 #include "library/blast/blast.h"
 #include "library/blast/simplifier/simplifier.h"
@@ -524,6 +525,23 @@ static void print_unification_hints(parser & p) {
     out << pp_unification_hints(hints, out.get_formatter(), header);
 }
 
+static void print_defeq_lemmas(parser & p) {
+    io_state_stream out = p.regular_stream();
+    defeq_simp_lemmas lemmas;
+    name ns;
+    if (p.curr_is_identifier()) {
+        ns = p.get_name_val();
+        p.next();
+        lemmas = get_defeq_simp_lemmas(p.env(), ns);
+    } else {
+        lemmas = get_defeq_simp_lemmas(p.env());
+    }
+    format header;
+    if (!ns.is_anonymous())
+        header = format(" at namespace '") + format(ns) + format("'");
+    out << pp_defeq_simp_lemmas(lemmas, out.get_formatter(), header);
+}
+
 static void print_simp_rules(parser & p) {
     io_state_stream out = p.regular_stream();
     blast::scope_debug scope(p.env(), p.ios());
@@ -720,6 +738,9 @@ environment print_cmd(parser & p) {
     } else if (p.curr_is_token(get_unify_attr_tk())) {
         p.next();
         print_unification_hints(p);
+    } else if (p.curr_is_token(get_defeq_attr_tk())) {
+        p.next();
+        print_defeq_lemmas(p);
     } else if (p.curr_is_token(get_simp_attr_tk())) {
         p.next();
         print_simp_rules(p);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index bd8616364..429d356c6 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -120,7 +120,8 @@ void init_token_table(token_table & t) {
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
          "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#simplify", "#app_builder", "#refl", "#symm",
-         "#trans", "#congr", "#hcongr", "#congr_simp", "#congr_rel", "#normalizer", "#abstract_expr", "#unify", nullptr};
+         "#trans", "#congr", "#hcongr", "#congr_simp", "#congr_rel", "#normalizer", "#abstract_expr", "#unify",
+         "#defeq_simplify", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 800a9d737..887965df3 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -120,6 +120,7 @@ static name const * g_intro_bang_attr_tk = nullptr;
 static name const * g_elim_attr_tk = nullptr;
 static name const * g_recursor_tk = nullptr;
 static name const * g_unify_attr_tk = nullptr;
+static name const * g_defeq_attr_tk = nullptr;
 static name const * g_attribute_tk = nullptr;
 static name const * g_with_tk = nullptr;
 static name const * g_class_tk = nullptr;
@@ -142,7 +143,6 @@ static name const * g_tactic_infixr_tk = nullptr;
 static name const * g_tactic_postfix_tk = nullptr;
 static name const * g_tactic_prefix_tk = nullptr;
 static name const * g_tactic_notation_tk = nullptr;
-static name const * g_call_tk = nullptr;
 static name const * g_calc_tk = nullptr;
 static name const * g_obtain_tk = nullptr;
 static name const * g_root_tk = nullptr;
@@ -271,6 +271,7 @@ void initialize_tokens() {
     g_elim_attr_tk = new name{"[elim]"};
     g_recursor_tk = new name{"[recursor"};
     g_unify_attr_tk = new name{"[unify]"};
+    g_defeq_attr_tk = new name{"[defeq]"};
     g_attribute_tk = new name{"attribute"};
     g_with_tk = new name{"with"};
     g_class_tk = new name{"[class]"};
@@ -293,7 +294,6 @@ void initialize_tokens() {
     g_tactic_postfix_tk = new name{"tactic_postfix"};
     g_tactic_prefix_tk = new name{"tactic_prefix"};
     g_tactic_notation_tk = new name{"tactic_notation"};
-    g_call_tk = new name{"call"};
     g_calc_tk = new name{"calc"};
     g_obtain_tk = new name{"obtain"};
     g_root_tk = new name{"_root_"};
@@ -423,6 +423,7 @@ void finalize_tokens() {
     delete g_elim_attr_tk;
     delete g_recursor_tk;
     delete g_unify_attr_tk;
+    delete g_defeq_attr_tk;
     delete g_attribute_tk;
     delete g_with_tk;
     delete g_class_tk;
@@ -445,7 +446,6 @@ void finalize_tokens() {
     delete g_tactic_postfix_tk;
     delete g_tactic_prefix_tk;
     delete g_tactic_notation_tk;
-    delete g_call_tk;
     delete g_calc_tk;
     delete g_obtain_tk;
     delete g_root_tk;
@@ -574,6 +574,7 @@ name const & get_intro_bang_attr_tk() { return *g_intro_bang_attr_tk; }
 name const & get_elim_attr_tk() { return *g_elim_attr_tk; }
 name const & get_recursor_tk() { return *g_recursor_tk; }
 name const & get_unify_attr_tk() { return *g_unify_attr_tk; }
+name const & get_defeq_attr_tk() { return *g_defeq_attr_tk; }
 name const & get_attribute_tk() { return *g_attribute_tk; }
 name const & get_with_tk() { return *g_with_tk; }
 name const & get_class_tk() { return *g_class_tk; }
@@ -596,7 +597,6 @@ name const & get_tactic_infixr_tk() { return *g_tactic_infixr_tk; }
 name const & get_tactic_postfix_tk() { return *g_tactic_postfix_tk; }
 name const & get_tactic_prefix_tk() { return *g_tactic_prefix_tk; }
 name const & get_tactic_notation_tk() { return *g_tactic_notation_tk; }
-name const & get_call_tk() { return *g_call_tk; }
 name const & get_calc_tk() { return *g_calc_tk; }
 name const & get_obtain_tk() { return *g_obtain_tk; }
 name const & get_root_tk() { return *g_root_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 791de64e9..5b081b2f6 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -122,6 +122,7 @@ name const & get_intro_bang_attr_tk();
 name const & get_elim_attr_tk();
 name const & get_recursor_tk();
 name const & get_unify_attr_tk();
+name const & get_defeq_attr_tk();
 name const & get_attribute_tk();
 name const & get_with_tk();
 name const & get_class_tk();
@@ -144,7 +145,6 @@ name const & get_tactic_infixr_tk();
 name const & get_tactic_postfix_tk();
 name const & get_tactic_prefix_tk();
 name const & get_tactic_notation_tk();
-name const & get_call_tk();
 name const & get_calc_tk();
 name const & get_obtain_tk();
 name const & get_root_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index 316214ae5..5742f9e73 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -115,6 +115,7 @@ intro_bang_attr [intro!]
 elim_attr    [elim]
 recursor     [recursor
 unify_attr   [unify]
+defeq_attr   [defeq]
 attribute    attribute
 with         with
 class        [class]
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index eddf9ea9b..b9466e89e 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -18,4 +18,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   aux_recursors.cpp norm_num.cpp norm_num.cpp class_instance_resolution.cpp type_context.cpp
   tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp
   abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp
-  attribute_manager.cpp error_handling.cpp unification_hint.cpp)
+  attribute_manager.cpp error_handling.cpp unification_hint.cpp defeq_simp_lemmas.cpp
+  defeq_simplifier.cpp)
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 84346f194..153de75d6 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -189,6 +189,7 @@ name const * g_prod_pr2 = nullptr;
 name const * g_propext = nullptr;
 name const * g_rat_divide = nullptr;
 name const * g_rat_of_num = nullptr;
+name const * g_rfl = nullptr;
 name const * g_right_distrib = nullptr;
 name const * g_ring = nullptr;
 name const * g_semiring = nullptr;
@@ -463,6 +464,7 @@ void initialize_constants() {
     g_propext = new name{"propext"};
     g_rat_divide = new name{"rat", "divide"};
     g_rat_of_num = new name{"rat", "of_num"};
+    g_rfl = new name{"rfl"};
     g_right_distrib = new name{"right_distrib"};
     g_ring = new name{"ring"};
     g_semiring = new name{"semiring"};
@@ -738,6 +740,7 @@ void finalize_constants() {
     delete g_propext;
     delete g_rat_divide;
     delete g_rat_of_num;
+    delete g_rfl;
     delete g_right_distrib;
     delete g_ring;
     delete g_semiring;
@@ -1012,6 +1015,7 @@ name const & get_prod_pr2_name() { return *g_prod_pr2; }
 name const & get_propext_name() { return *g_propext; }
 name const & get_rat_divide_name() { return *g_rat_divide; }
 name const & get_rat_of_num_name() { return *g_rat_of_num; }
+name const & get_rfl_name() { return *g_rfl; }
 name const & get_right_distrib_name() { return *g_right_distrib; }
 name const & get_ring_name() { return *g_ring; }
 name const & get_semiring_name() { return *g_semiring; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 9fccbe000..5f926c1e9 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -191,6 +191,7 @@ name const & get_prod_pr2_name();
 name const & get_propext_name();
 name const & get_rat_divide_name();
 name const & get_rat_of_num_name();
+name const & get_rfl_name();
 name const & get_right_distrib_name();
 name const & get_ring_name();
 name const & get_semiring_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index de299eed7..2b234a4f8 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -184,6 +184,7 @@ prod.pr2
 propext
 rat.divide
 rat.of_num
+rfl
 right_distrib
 ring
 semiring
diff --git a/src/library/defeq_simp_lemmas.cpp b/src/library/defeq_simp_lemmas.cpp
new file mode 100644
index 000000000..85d3765bb
--- /dev/null
+++ b/src/library/defeq_simp_lemmas.cpp
@@ -0,0 +1,191 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include <string>
+#include "util/sexpr/format.h"
+#include "kernel/expr.h"
+#include "kernel/error_msgs.h"
+#include "kernel/instantiate.h"
+#include "library/attribute_manager.h"
+#include "library/constants.h"
+#include "library/defeq_simp_lemmas.h"
+#include "library/util.h"
+#include "library/expr_lt.h"
+#include "library/scoped_ext.h"
+#include "library/tmp_type_context.h"
+
+namespace lean {
+
+/* defeq simp lemmas  */
+
+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):
+    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) {
+    return sl1.get_lhs() == sl2.get_lhs() && sl1.get_rhs() == sl2.get_rhs();
+}
+
+/* Environment extension */
+
+static name * g_class_name = nullptr;
+static std::string * g_key = nullptr;
+
+struct defeq_simp_lemmas_state {
+    defeq_simp_lemmas m_defeq_simp_lemmas;
+    name_map<unsigned> m_decl_name_to_prio; // Note: redundant but convenient
+
+    void register_defeq_simp_lemma(tmp_type_context & tctx, name const & decl_name, unsigned priority) {
+        declaration const & d = tctx.env().get(decl_name);
+        // TODO(dhs): once we refactor to register this attribute as "definitions-only", this can be an assert
+        if (!d.is_definition()) {
+            throw exception("invalid [defeq] simp lemma: must be a definition so that definitional equality can be verified");
+        }
+        buffer<level> us;
+        unsigned num_univs = d.get_num_univ_params();
+        for (unsigned i = 0; i < num_univs; i++) {
+            us.push_back(tctx.mk_uvar());
+        }
+        levels ls = to_list(us);
+        expr type    = instantiate_type_univ_params(d, ls);
+        expr proof   = instantiate_value_univ_params(d, ls);
+        return register_defeq_simp_lemma_core(tctx, decl_name, ls, type, proof, priority);
+    }
+
+    void register_defeq_simp_lemma_core(tmp_type_context & tctx, name const & decl_name, levels const & umetas,
+                                        expr const & type, expr const & proof, unsigned priority) {
+        m_decl_name_to_prio.insert(decl_name, priority);
+        expr rule = type;
+        expr pf = proof;
+        buffer<expr> emetas;
+        buffer<bool> instances;
+        while (is_pi(rule)) {
+            expr mvar = tctx.mk_mvar(binding_domain(rule));
+            emetas.push_back(mvar);
+            instances.push_back(binding_info(rule).is_inst_implicit());
+            rule = instantiate(binding_body(rule), mvar);
+            pf = binding_body(pf);
+        }
+        expr lhs, rhs;
+        if (!is_eq(rule, lhs, rhs))
+            throw exception("invalid [defeq] simp 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 exception("invalid [defeq] simp lemma: proof must be an application of either 'eq.refl' or 'rfl' to two arguments");
+        if (lhs == rhs)
+            throw exception("invalid [defeq] simp lemma: the two sides of the equality cannot be structurally equal");
+        defeq_simp_lemma lemma(decl_name, umetas, to_list(emetas), to_list(instances), lhs, rhs, priority);
+        m_defeq_simp_lemmas.insert(lhs, lemma);
+    }
+};
+
+struct defeq_simp_lemmas_entry {
+    name m_decl_name;
+    unsigned m_priority;
+    defeq_simp_lemmas_entry(name const & decl_name, unsigned priority):
+        m_decl_name(decl_name), m_priority(priority) {}
+};
+
+struct defeq_simp_lemmas_config {
+    typedef defeq_simp_lemmas_entry entry;
+    typedef defeq_simp_lemmas_state state;
+
+    static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) {
+        tmp_type_context tctx(env, ios.get_options());
+        s.register_defeq_simp_lemma(tctx, e.m_decl_name, e.m_priority);
+    }
+    static name const & get_class_name() {
+        return *g_class_name;
+    }
+    static std::string const & get_serialization_key() {
+        return *g_key;
+    }
+    static void  write_entry(serializer & s, entry const & e) {
+        s << e.m_decl_name << e.m_priority;
+    }
+    static entry read_entry(deserializer & d) {
+        name decl_name; unsigned prio;
+        d >> decl_name >> prio;
+        return entry(decl_name, prio);
+    }
+    static optional<unsigned> get_fingerprint(entry const & e) {
+        return some(hash(e.m_decl_name.hash(), e.m_priority));
+    }
+};
+
+typedef scoped_ext<defeq_simp_lemmas_config> defeq_simp_lemmas_ext;
+
+environment add_defeq_simp_lemma(environment const & env, io_state const & ios, name const & decl_name, unsigned prio, name const & ns, bool persistent) {
+    return defeq_simp_lemmas_ext::add_entry(env, ios, defeq_simp_lemmas_entry(decl_name, prio), ns, persistent);
+}
+
+bool is_defeq_simp_lemma(environment const & env, name const & decl_name) {
+    return defeq_simp_lemmas_ext::get_state(env).m_decl_name_to_prio.contains(decl_name);
+}
+
+defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env) {
+    return defeq_simp_lemmas_ext::get_state(env).m_defeq_simp_lemmas;
+}
+
+defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env, name const & ns) {
+    list<defeq_simp_lemmas_entry> const * entries = defeq_simp_lemmas_ext::get_entries(env, ns);
+    defeq_simp_lemmas_state s;
+    if (entries) {
+        for (auto const & e : *entries) {
+            tmp_type_context tctx(env, get_dummy_ios().get_options());
+            s.register_defeq_simp_lemma(tctx, e.m_decl_name, e.m_priority);
+        }
+    }
+    return s.m_defeq_simp_lemmas;
+}
+
+/* Pretty printing */
+
+format defeq_simp_lemma::pp(formatter const & fmt) const {
+    format r;
+    r += format("#") + format(get_num_emeta());
+    if (get_priority() != LEAN_DEFAULT_PRIORITY)
+        r += space() + paren(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 const & header) {
+    format r;
+    r += format("defeq simp lemmas");
+    r += header + colon() + line();
+    lemmas.for_each_entry([&](head_index const &, defeq_simp_lemma const & lemma) {
+             r += lemma.pp(fmt) + line();
+        });
+    return r;
+}
+
+/* Setup and teardown */
+
+void initialize_defeq_simp_lemmas() {
+    g_class_name    = new name("defeq_simp_lemmas");
+    g_key           = new std::string("DEFEQ_SIMP_LEMMAS");
+
+    defeq_simp_lemmas_ext::initialize();
+
+    register_prio_attribute("defeq", "defeq simp lemma",
+                            add_defeq_simp_lemma,
+                            is_defeq_simp_lemma,
+                            [](environment const & env, name const & decl_name) {
+                                if (auto p = defeq_simp_lemmas_ext::get_state(env).m_decl_name_to_prio.find(decl_name))
+                                    return *p;
+                                else
+                                    return LEAN_DEFAULT_PRIORITY;
+                            });
+}
+
+void finalize_defeq_simp_lemmas() {
+    defeq_simp_lemmas_ext::finalize();
+    delete g_key;
+    delete g_class_name;
+}
+
+}
diff --git a/src/library/defeq_simp_lemmas.h b/src/library/defeq_simp_lemmas.h
new file mode 100644
index 000000000..2aa2ee945
--- /dev/null
+++ b/src/library/defeq_simp_lemmas.h
@@ -0,0 +1,58 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+#include "kernel/environment.h"
+#include "library/io_state.h"
+#include "library/head_map.h"
+
+namespace lean {
+
+class defeq_simp_lemma {
+    name                m_id;
+    levels              m_umetas;
+    list<expr>          m_emetas;
+    list<bool>          m_instances;
+
+    expr                m_lhs;
+    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);
+
+    name const & get_id() const { return m_id; }
+    unsigned get_num_umeta() const { return length(m_umetas); }
+    unsigned get_num_emeta() const { return length(m_emetas); }
+
+    /** \brief Return a list containing the expression metavariables in reverse order. */
+    list<expr> const & get_emetas() const { return m_emetas; }
+
+    /** \brief Return a list of bools indicating whether or not each expression metavariable
+        in <tt>get_emetas()</tt> is an instance. */
+    list<bool> const & get_instances() const { return m_instances; }
+
+    expr const & get_lhs() const { return m_lhs; }
+    expr const & get_rhs() const { return m_rhs; }
+
+    unsigned get_priority() const { return m_priority; }
+    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); }
+
+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;
+
+defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env);
+defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env, name const & ns);
+
+format pp_defeq_simp_lemmas(defeq_simp_lemmas const & lemmas, formatter const & fmt, format const & header);
+
+void initialize_defeq_simp_lemmas();
+void finalize_defeq_simp_lemmas();
+}
diff --git a/src/library/defeq_simplifier.cpp b/src/library/defeq_simplifier.cpp
new file mode 100644
index 000000000..ad611c010
--- /dev/null
+++ b/src/library/defeq_simplifier.cpp
@@ -0,0 +1,312 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include "library/defeq_simplifier.h"
+#include "util/interrupt.h"
+#include "util/sexpr/option_declarations.h"
+#include "kernel/expr_maps.h"
+#include "kernel/instantiate.h"
+#include "kernel/abstract.h"
+#include "library/trace.h"
+#include "library/tmp_type_context.h"
+#include "library/normalize.h"
+
+#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS
+#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS 1000
+#endif
+#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS
+#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS 1000
+#endif
+#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN
+#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN false
+#endif
+#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXHAUSTIVE
+#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXHAUSTIVE true
+#endif
+#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE
+#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE true
+#endif
+#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS
+#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS false
+#endif
+
+namespace lean {
+
+/* Options */
+
+static name * g_simplify_max_simp_rounds     = nullptr;
+static name * g_simplify_max_rewrite_rounds  = nullptr;
+static name * g_simplify_top_down            = nullptr;
+static name * g_simplify_exhaustive          = nullptr;
+static name * g_simplify_memoize             = nullptr;
+static name * g_simplify_expand_macros       = nullptr;
+
+static unsigned get_simplify_max_simp_rounds(options const & o) {
+    return o.get_unsigned(*g_simplify_max_simp_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS);
+}
+
+static unsigned get_simplify_max_rewrite_rounds(options const & o) {
+    return o.get_unsigned(*g_simplify_max_rewrite_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS);
+}
+
+static bool get_simplify_top_down(options const & o) {
+    return o.get_bool(*g_simplify_top_down, LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN);
+}
+
+static bool get_simplify_exhaustive(options const & o) {
+    return o.get_bool(*g_simplify_exhaustive, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXHAUSTIVE);
+}
+
+static bool get_simplify_memoize(options const & o) {
+    return o.get_bool(*g_simplify_memoize, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE);
+}
+
+static bool get_simplify_expand_macros(options const & o) {
+    return o.get_bool(*g_simplify_expand_macros, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS);
+}
+
+/* Main simplifier class */
+
+class defeq_simplify_fn {
+    tmp_type_context                  m_tmp_tctx;
+    defeq_simp_lemmas                 m_simp_lemmas;
+
+    unsigned                          m_num_simp_rounds{0};
+    unsigned                          m_num_rewrite_rounds{0};
+
+    options const &                   m_options;
+
+    /* Options */
+    unsigned                          m_max_simp_rounds;
+    unsigned                          m_max_rewrite_rounds;
+    bool                              m_top_down;
+    bool                              m_exhaustive;
+    bool                              m_memoize;
+    bool                              m_expand_macros;
+
+    /* Cache */
+    expr_struct_map<expr>             m_cache;
+
+    optional<expr> cache_lookup(expr const & e) {
+        auto it = m_cache.find(e);
+        if (it == m_cache.end()) return none_expr();
+        else return some_expr(it->second);
+    }
+
+    void cache_save(expr const & e, expr const & e_simp) {
+        m_cache.insert(mk_pair(e, e_simp));
+    }
+
+    /* Simplification */
+    expr defeq_simplify(expr const & _e) {
+        expr e = _e;
+        lean_trace_inc_depth("defeq_simplifier");
+        lean_trace_d("defeq_simplifier", tout() << e << "\n";);
+
+        while (true) {
+            expr e_start = e;
+
+            check_system("defeq_simplifier");
+            m_num_simp_rounds++;
+            if (m_num_simp_rounds > m_max_simp_rounds)
+                throw exception("defeq_simplifier failed, maximum number of simp rounds exceeded");
+
+            if (m_memoize) {
+                if (auto it = cache_lookup(e)) return *it;
+            }
+
+            if (m_top_down) e = rewrite(whnf_eta(e));
+            e = whnf_eta(e);
+
+            switch (e.kind()) {
+            case expr_kind::Local:
+            case expr_kind::Meta:
+            case expr_kind::Sort:
+            case expr_kind::Constant:
+                break;
+            case expr_kind::Var:
+                lean_unreachable();
+            case expr_kind::Macro:
+                if (m_expand_macros) {
+                    if (auto m = m_tmp_tctx.expand_macro(e)) e = defeq_simplify(whnf_eta(*m));
+                }
+                break;
+            case expr_kind::Lambda:
+            case expr_kind::Pi:
+                e = defeq_simplify_binding(e);
+                break;
+            case expr_kind::App:
+                e = defeq_simplify_app(e);
+                break;
+            }
+
+            if (!m_top_down) e = rewrite(whnf_eta(e));
+            if (!m_exhaustive || e == e_start) break;
+        }
+        if (m_memoize) cache_save(_e, e);
+        return e;
+    }
+
+    expr defeq_simplify_binding(expr const & e) {
+        expr d = defeq_simplify(binding_domain(e));
+        expr l = m_tmp_tctx.mk_tmp_local(binding_name(e), d, binding_info(e));
+        expr b = abstract(defeq_simplify(instantiate(binding_body(e), l)), l);
+        return update_binding(e, d, b);
+    }
+
+    expr defeq_simplify_app(expr const & e) {
+        buffer<expr> args;
+        expr f = defeq_simplify(get_app_args(e, args));
+        for (unsigned i = 0; i < args.size(); ++i) args[i] = defeq_simplify(args[i]);
+        return mk_app(f, args);
+    }
+
+    /* Rewriting */
+    expr rewrite(expr const & _e) {
+        expr e = _e;
+        while (true) {
+            check_system("defeq_simplifier");
+
+            m_num_rewrite_rounds++;
+            if (m_num_rewrite_rounds > m_max_rewrite_rounds)
+                throw exception("defeq_simplifier failed, maximum number of rewrite rounds exceeded");
+
+            list<defeq_simp_lemma> const * simp_lemmas_ptr = m_simp_lemmas.find(e);
+            if (!simp_lemmas_ptr) return e;
+            buffer<defeq_simp_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);
+            if (e == e_start) break;
+        }
+        return e;
+    }
+
+    expr rewrite(expr const & e, defeq_simp_lemma const & sl) {
+        tmp_type_context tmp_tctx(m_tmp_tctx.env(), m_options);
+        tmp_tctx.clear();
+        tmp_tctx.set_next_uvar_idx(sl.get_num_umeta());
+        tmp_tctx.set_next_mvar_idx(sl.get_num_emeta());
+
+        if (!tmp_tctx.is_def_eq(e, sl.get_lhs())) return e;
+
+        lean_trace(name({"defeq_simplifier", "rewrite"}),
+                   expr new_lhs = tmp_tctx.instantiate_uvars_mvars(sl.get_lhs());
+                   expr new_rhs = tmp_tctx.instantiate_uvars_mvars(sl.get_rhs());
+                   tout() << "(" << sl.get_id() << ") "
+                   << "[" << new_lhs << " --> " << new_rhs << "]\n";);
+
+        if (!instantiate_emetas(tmp_tctx, sl.get_emetas(), sl.get_instances())) return e;
+
+        for (unsigned i = 0; i < sl.get_num_umeta(); i++) {
+            if (!tmp_tctx.is_uvar_assigned(i)) return e;
+        }
+
+        expr new_rhs = tmp_tctx.instantiate_uvars_mvars(sl.get_rhs());
+        return new_rhs;
+    }
+
+
+    bool instantiate_emetas(tmp_type_context & tmp_tctx, list<expr> const & _emetas, list<bool> const & _instances) {
+        buffer<expr> emetas;
+        buffer<bool> instances;
+        to_buffer(_emetas, emetas);
+        to_buffer(_instances, instances);
+
+        lean_assert(emetas.size() == instances.size());
+        for (unsigned i = 0; i < emetas.size(); ++i) {
+            expr m = emetas[i];
+            unsigned mvar_idx = emetas.size() - 1 - i;
+            expr m_type = tmp_tctx.instantiate_uvars_mvars(tmp_tctx.infer(m));
+            lean_assert(!has_metavar(m_type));
+            if (tmp_tctx.is_mvar_assigned(mvar_idx)) continue;
+            if (instances[i]) {
+                if (auto v = tmp_tctx.mk_class_instance(m_type)) {
+                    if (!tmp_tctx.assign(m, *v)) {
+                        lean_trace(name({"defeq_simplifier", "failure"}),
+                                   tout() << "unable to assign instance for: " << m_type << "\n";);
+                        return false;
+                    } else {
+                        lean_assert(tmp_tctx.is_mvar_assigned(mvar_idx));
+                        continue;
+                    }
+                } else {
+                    lean_trace(name({"defeq_simplifier", "failure"}),
+                               tout() << "unable to synthesize instance for: " << m_type << "\n";);
+                    return false;
+                }
+            } else {
+                lean_trace(name({"defeq_simplifier", "failure"}),
+                           tout() << "failed to assign: " << m << " : " << m_type << "\n";);
+                return false;
+            }
+        }
+        return true;
+    }
+
+    expr whnf_eta(expr const & e) {
+        return try_eta(m_tmp_tctx.whnf(e));
+    }
+
+public:
+    defeq_simplify_fn(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas):
+        m_tmp_tctx(env, o),
+        m_simp_lemmas(simp_lemmas),
+        m_options(o),
+        m_max_simp_rounds(get_simplify_max_simp_rounds(o)),
+        m_max_rewrite_rounds(get_simplify_max_rewrite_rounds(o)),
+        m_top_down(get_simplify_top_down(o)),
+        m_exhaustive(get_simplify_exhaustive(o)),
+        m_memoize(get_simplify_memoize(o)),
+        m_expand_macros(get_simplify_expand_macros(o)) {}
+
+    expr operator()(expr const & e)  { return defeq_simplify(e); }
+};
+
+/* Setup and teardown */
+
+void initialize_defeq_simplifier() {
+    register_trace_class("defeq_simplifier");
+    register_trace_class(name({"defeq_simplifier", "rewrite"}));
+    register_trace_class(name({"defeq_simplifier", "failure"}));
+
+    g_simplify_max_simp_rounds    = new name{"defeq_simplify", "max_simp_rounds"};
+    g_simplify_max_rewrite_rounds = new name{"defeq_simplify", "max_rewrite_rounds"};
+    g_simplify_top_down           = new name{"defeq_simplify", "top_down"};
+    g_simplify_exhaustive         = new name{"defeq_simplify", "exhaustive"};
+    g_simplify_memoize            = new name{"defeq_simplify", "memoize"};
+    g_simplify_expand_macros      = new name{"defeq_simplify", "expand_macros"};
+
+    register_unsigned_option(*g_simplify_max_simp_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS,
+                             "(defeq_simplify) max allowed simplification rounds");
+    register_unsigned_option(*g_simplify_max_rewrite_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS,
+                             "(defeq_simplify) max allowed rewrite rounds");
+    register_bool_option(*g_simplify_top_down, LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN,
+                         "(defeq_simplify) use top-down rewriting instead of bottom-up");
+    register_bool_option(*g_simplify_exhaustive, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXHAUSTIVE,
+                         "(defeq_simplify) simplify exhaustively");
+    register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE,
+                         "(defeq_simplify) memoize simplifications");
+    register_bool_option(*g_simplify_expand_macros, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS,
+                         "(defeq_simplify) expand macros");
+}
+
+void finalize_defeq_simplifier() {
+    delete g_simplify_expand_macros;
+    delete g_simplify_memoize;
+    delete g_simplify_exhaustive;
+    delete g_simplify_top_down;
+    delete g_simplify_max_rewrite_rounds;
+    delete g_simplify_max_simp_rounds;
+}
+
+/* Entry point */
+expr defeq_simplify(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e) {
+    return defeq_simplify_fn(env, o, simp_lemmas)(e);
+}
+
+
+}
diff --git a/src/library/defeq_simplifier.h b/src/library/defeq_simplifier.h
new file mode 100644
index 000000000..849686ffb
--- /dev/null
+++ b/src/library/defeq_simplifier.h
@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+#include "kernel/expr.h"
+#include "library/defeq_simp_lemmas.h"
+
+namespace lean {
+
+expr defeq_simplify(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e);
+
+void initialize_defeq_simplifier();
+void finalize_defeq_simplifier();
+
+}
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 5318016b1..cc4d0fa86 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -48,6 +48,8 @@ Author: Leonardo de Moura
 #include "library/attribute_manager.h"
 #include "library/fun_info_manager.h"
 #include "library/unification_hint.h"
+#include "library/defeq_simp_lemmas.h"
+#include "library/defeq_simplifier.h"
 
 namespace lean {
 void initialize_library_module() {
@@ -95,9 +97,13 @@ void initialize_library_module() {
     initialize_app_builder();
     initialize_fun_info_manager();
     initialize_unification_hint();
+    initialize_defeq_simp_lemmas();
+    initialize_defeq_simplifier();
 }
 
 void finalize_library_module() {
+    finalize_defeq_simplifier();
+    finalize_defeq_simp_lemmas();
     finalize_unification_hint();
     finalize_fun_info_manager();
     finalize_app_builder();
diff --git a/tests/lean/defeq_simp_lemmas1.lean b/tests/lean/defeq_simp_lemmas1.lean
new file mode 100644
index 000000000..6679295fe
--- /dev/null
+++ b/tests/lean/defeq_simp_lemmas1.lean
@@ -0,0 +1,15 @@
+universe l
+constants (A : Type.{l})
+
+definition q (x : A) := x
+definition h (x : A) : A := q x
+definition g (x y : A) := h y
+definition f (x y z : A) := g (g x y) z
+definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z)
+
+definition h.def [defeq] (x : A) : h x = q x := rfl
+definition g.def [defeq] (x y : A) : g x y = h y := rfl
+definition f.def [defeq] (x y z : A) : f x y z = g (g x y) z := rfl
+definition d.def [defeq] (x y z w : A) : d x y z w = f (f x y z) (f y z w) (f x w z) := rfl
+
+print [defeq]
diff --git a/tests/lean/defeq_simp_lemmas1.lean.expected.out b/tests/lean/defeq_simp_lemmas1.lean.expected.out
new file mode 100644
index 000000000..30dba9002
--- /dev/null
+++ b/tests/lean/defeq_simp_lemmas1.lean.expected.out
@@ -0,0 +1,5 @@
+defeq simp lemmas:
+#2, g ?M_1 ?M_2 ↦ h ?M_2
+#4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
+#3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
+#1, h ?M_1 ↦ q ?M_1
diff --git a/tests/lean/defeq_simp_lemmas2.lean b/tests/lean/defeq_simp_lemmas2.lean
new file mode 100644
index 000000000..a9e5ff29c
--- /dev/null
+++ b/tests/lean/defeq_simp_lemmas2.lean
@@ -0,0 +1,37 @@
+universe l
+constants (A : Type.{l})
+
+definition q (x : A) := x
+definition h (x : A) : A := q x
+definition g (x y : A) := h y
+definition f (x y z : A) := g (g x y) z
+definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z)
+
+definition h.rfl [defeq] (x : A) : h x = x := rfl
+definition g.rfl [defeq] (x y : A) : g x y = y := rfl
+definition f.rfl [defeq] (x y z : A) : f x y z = z := rfl
+definition d.rfl [defeq] (x y z w : A) : d x y z w = z := rfl
+
+definition h.def [defeq] (x : A) : h x = q x := rfl
+definition g.def [defeq] (x y : A) : g x y = h y := rfl
+definition f.def [defeq] (x y z : A) : f x y z = g (g x y) z := rfl
+definition d.def [defeq] (x y z w : A) : d x y z w = f (f x y z) (f y z w) (f x w z) := rfl
+
+-- Confirm that more recent annotations get priority
+print [defeq]
+
+attribute h.rfl [defeq] [priority 1001]
+attribute g.rfl [defeq] [priority 1001]
+attribute f.rfl [defeq] [priority 1001]
+attribute d.rfl [defeq] [priority 1001]
+
+-- Confirm that priority annotations override
+print [defeq]
+
+attribute h.def [defeq] [priority 1001]
+attribute g.def [defeq] [priority 1001]
+attribute f.def [defeq] [priority 1001]
+attribute d.def [defeq] [priority 1001]
+
+-- Confirm that most recent annotations get priority to break explicit priority ties
+print [defeq]
diff --git a/tests/lean/defeq_simp_lemmas2.lean.expected.out b/tests/lean/defeq_simp_lemmas2.lean.expected.out
new file mode 100644
index 000000000..8f7e13230
--- /dev/null
+++ b/tests/lean/defeq_simp_lemmas2.lean.expected.out
@@ -0,0 +1,27 @@
+defeq simp lemmas:
+#2, g ?M_1 ?M_2 ↦ h ?M_2
+#2, g ?M_1 ?M_2 ↦ ?M_2
+#4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
+#4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3
+#3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
+#3, f ?M_1 ?M_2 ?M_3 ↦ ?M_3
+#1, h ?M_1 ↦ q ?M_1
+#1, h ?M_1 ↦ ?M_1
+defeq simp lemmas:
+#2 (1001), g ?M_1 ?M_2 ↦ ?M_2
+#2, g ?M_1 ?M_2 ↦ h ?M_2
+#4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3
+#4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
+#3 (1001), f ?M_1 ?M_2 ?M_3 ↦ ?M_3
+#3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
+#1 (1001), h ?M_1 ↦ ?M_1
+#1, h ?M_1 ↦ q ?M_1
+defeq simp lemmas:
+#2 (1001), g ?M_1 ?M_2 ↦ h ?M_2
+#2 (1001), g ?M_1 ?M_2 ↦ ?M_2
+#4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
+#4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3
+#3 (1001), f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
+#3 (1001), f ?M_1 ?M_2 ?M_3 ↦ ?M_3
+#1 (1001), h ?M_1 ↦ q ?M_1
+#1 (1001), h ?M_1 ↦ ?M_1
diff --git a/tests/lean/defeq_simplifier1.lean b/tests/lean/defeq_simplifier1.lean
new file mode 100644
index 000000000..03cf70104
--- /dev/null
+++ b/tests/lean/defeq_simplifier1.lean
@@ -0,0 +1,30 @@
+universe l
+constants (A : Type.{l})
+
+definition q (x : A) : A := x
+definition h (x : A) : A := q x
+definition g (x y : A) := h y
+definition f (x y z : A) := g (g x y) z
+definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z)
+
+definition h.def [defeq] (x : A) : h x = q x := rfl
+definition g.def [defeq] (x y : A) : g x y = h y := rfl
+definition f.def [defeq] (x y z : A) : f x y z = g (g x y) z := rfl
+definition d.def [defeq] (x y z w : A) : d x y z w = f (f x y z) (f y z w) (f x w z) := rfl
+
+#defeq_simplify env λ x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z))
+#defeq_simplify env Π x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z)) = (λ x, x) w
+
+set_option defeq_simplify.exhaustive false
+#defeq_simplify env λ x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z))
+#defeq_simplify env Π x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z)) = (λ x, x) w
+
+set_option defeq_simplify.top_down true
+#defeq_simplify env λ x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z))
+#defeq_simplify env Π x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z)) = (λ x, x) w
+
+attribute q [reducible]
+set_option defeq_simplify.exhaustive true
+set_option defeq_simplify.top_down false
+#defeq_simplify env λ x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z))
+#defeq_simplify env Π x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z)) = (λ x, x) w
diff --git a/tests/lean/defeq_simplifier1.lean.expected.out b/tests/lean/defeq_simplifier1.lean.expected.out
new file mode 100644
index 000000000..e1d570060
--- /dev/null
+++ b/tests/lean/defeq_simplifier1.lean.expected.out
@@ -0,0 +1,8 @@
+λ (x y z w : A), q (q (q w))
+A → A → A → (∀ (w : A), q (q (q w)) = w)
+λ (x y z w : A), q (f (q (q x)) (q (q z)) (q w))
+∀ (x : A), A → (∀ (z w : A), q (f (q (q x)) (q (q z)) (q w)) = w)
+λ (x y z w : A), q (q (q w))
+A → A → A → (∀ (w : A), q (q (q w)) = w)
+λ (x y z w : A), w
+A → A → A → (∀ (w : A), w = w)