diff --git a/library/init/cc_lemmas.lean b/library/init/cc_lemmas.lean
new file mode 100644
index 0000000000..642a59cea1
--- /dev/null
+++ b/library/init/cc_lemmas.lean
@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.propext init.classical
+
+/- Lemmas use by the congruence closure module -/
+
+lemma iff_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a ↔ b) = b :=
+h^.symm ▸ propext (true_iff _)
+
+lemma iff_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a ↔ b) = a :=
+h^.symm ▸ propext (iff_true _)
+lemma iff_eq_true_of_eq {a b : Prop} (h : a = b) : (a ↔ b) = true :=
+h ▸ propext (iff_self _)
+
+lemma and_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a ∧ b) = b :=
+h^.symm ▸ propext (true_and  _)
+
+lemma and_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a ∧ b) = a :=
+h^.symm ▸ propext (and_true _)
+
+lemma and_eq_of_eq_false_left {a b : Prop} (h : a = false) : (a ∧ b) = false :=
+h^.symm ▸ propext (false_and _)
+
+lemma and_eq_of_eq_false_right {a b : Prop} (h : b = false) : (a ∧ b) = false :=
+h^.symm ▸ propext (and_false _)
+
+lemma and_eq_of_eq {a b : Prop} (h : a = b) : (a ∧ b) = a :=
+h ▸ propext (and_self _)
+
+lemma or_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a ∨ b) = true :=
+h^.symm ▸ propext (true_or  _)
+
+lemma or_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a ∨ b) = true :=
+h^.symm ▸ propext (or_true _)
+
+lemma or_eq_of_eq_false_left {a b : Prop} (h : a = false) : (a ∨ b) = b :=
+h^.symm ▸ propext (false_or _)
+
+lemma or_eq_of_eq_false_right {a b : Prop} (h : b = false) : (a ∨ b) = a :=
+h^.symm ▸ propext (or_false _)
+
+lemma or_eq_of_eq {a b : Prop} (h : a = b) : (a ∨ b) = a :=
+h ▸ propext (or_self _)
+
+lemma imp_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a → b) = b :=
+h^.symm ▸ propext (iff.intro (λ h, h trivial) (λ h₁ h₂, h₁))
+
+lemma imp_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a → b) = true :=
+h^.symm ▸ propext (iff.intro (λ h, trivial) (λ h₁ h₂, h₁))
+
+lemma imp_eq_of_eq_false_left {a b : Prop} (h : a = false) : (a → b) = true :=
+h^.symm ▸ propext (iff.intro (λ h, trivial) (λ h₁ h₂, false.elim h₂))
+
+lemma imp_eq_true_of_eq {a b : Prop} (h : a = b) : (a → b) = true :=
+h ▸ propext (iff.intro (λ h, trivial) (λ h ha, ha))
+
+lemma not_eq_of_eq_true {a : Prop} (h : a = true) : (not a) = false :=
+h^.symm ▸ propext not_true_iff
+
+lemma not_eq_of_eq_false {a : Prop} (h : a = false) : (not a) = true :=
+h^.symm ▸ propext not_false_iff
+
+lemma false_of_a_eq_not_a {a : Prop} (h : a = not a) : false :=
+have not a, from λ ha, absurd ha (eq.mp h ha),
+absurd (eq.mpr h this) this
+
+universe variables u
+
+lemma if_eq_of_eq_true {c : Prop} [d : decidable c] {α : Type u} (t e : α) (h : c = true) : (@ite c d α t e) = t :=
+if_pos (of_eq_true h)
+
+lemma if_eq_of_eq_false {c : Prop} [d : decidable c] {α : Type u} (t e : α) (h : c = false) : (@ite c d α t e) = e :=
+if_neg (not_of_eq_false h)
+
+lemma if_eq_of_eq (c : Prop) [d : decidable c] {α : Type u} {t e : α} (h : t = e) : (@ite c d α t e) = t :=
+match d with
+| (is_true hc)   := rfl
+| (is_false hnc) := eq.symm h
+end
+
+lemma eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = true) : a = true :=
+eq_true_intro (and.left (of_eq_true h))
+
+lemma eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = true) : b = true :=
+eq_true_intro (and.right (of_eq_true h))
+
+lemma eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = false) : a = false :=
+eq_false_intro (λ ha, false.elim (eq.mp h (or.inl ha)))
+
+lemma eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = false) : b = false :=
+eq_false_intro (λ hb, false.elim (eq.mp h (or.inr hb)))
+
+lemma eq_false_of_not_eq_true {a : Prop} (h : (not a) = true) : a = false :=
+eq_false_intro (λ ha, absurd ha (eq.mpr h trivial))
+
+/- Remark: the congruence closure module will only use the following lemma is
+   cc_config.em is tt. -/
+lemma eq_true_of_not_eq_false {a : Prop} (h : (not a) = false) : a = true :=
+eq_true_intro (classical.by_contradiction (λ hna, eq.mp h hna))
diff --git a/library/init/default.lean b/library/init/default.lean
index 91c19edff5..ec86e1ba39 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.core init.logic init.category init.data.basic
-import init.propext init.funext init.category.combinators init.function init.classical
+import init.propext init.cc_lemmas init.funext init.category.combinators init.function init.classical
 import init.util init.coe init.wf init.meta init.algebra init.data
 import init.native
 
diff --git a/library/init/meta/congruence_tactics.lean b/library/init/meta/congruence_tactics.lean
index 3c1477fe94..7603de95b3 100644
--- a/library/init/meta/congruence_tactics.lean
+++ b/library/init/meta/congruence_tactics.lean
@@ -16,9 +16,12 @@ structure cc_config :=
    "Congruence Closure in Intensional Type Theory". If ho_fns is none, then full support is provided
    for *all* constants. -/
 (ho_fns           : option (list name))
+/- If true, then use excluded middle -/
+(em               : bool)
+
 
 def default_cc_config : cc_config :=
-{ignore_instances := tt, ac := tt, ho_fns := some []}
+{ignore_instances := tt, ac := tt, ho_fns := some [], em := tt}
 
 /- Congruence closure state -/
 meta constant cc_state                  : Type
diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean
index 4f680f3371..2755361d37 100644
--- a/library/init/meta/default.lean
+++ b/library/init/meta/default.lean
@@ -14,4 +14,4 @@ import init.meta.mk_dec_eq_instance init.meta.mk_inhabited_instance
 import init.meta.simp_tactic init.meta.set_get_option_tactics
 import init.meta.interactive init.meta.converter init.meta.vm
 import init.meta.comp_value_tactics init.meta.congruence_tactics
-import init.meta.smt_tactic
+import init.meta.smt_tactic init.cc_lemmas
diff --git a/src/library/tactic/smt/CMakeLists.txt b/src/library/tactic/smt/CMakeLists.txt
index c82193de99..2403bfdd3e 100644
--- a/src/library/tactic/smt/CMakeLists.txt
+++ b/src/library/tactic/smt/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_library(smt OBJECT congruence_closure.cpp congruence_tactics.cpp
   hinst_lemmas.cpp ematch.cpp theory_ac.cpp util.cpp
-  unit_propagation.cpp smt_state.cpp init_module.cpp)
+  smt_state.cpp init_module.cpp)
diff --git a/src/library/tactic/smt/congruence_closure.cpp b/src/library/tactic/smt/congruence_closure.cpp
index 50aed23384..b5691c0a75 100644
--- a/src/library/tactic/smt/congruence_closure.cpp
+++ b/src/library/tactic/smt/congruence_closure.cpp
@@ -429,6 +429,14 @@ void congruence_closure::push_todo(expr const & lhs, expr const & rhs, expr cons
     m_todo.emplace_back(lhs, rhs, H, heq_proof);
 }
 
+void congruence_closure::push_heq(expr const & lhs, expr const & rhs, expr const & H) {
+    m_todo.emplace_back(lhs, rhs, H, true);
+}
+
+void congruence_closure::push_eq(expr const & lhs, expr const & rhs, expr const & H) {
+    m_todo.emplace_back(lhs, rhs, H, false);
+}
+
 void congruence_closure::process_subsingleton_elem(expr const & e) {
     expr type = m_ctx.infer(e);
     optional<expr> ss = m_ctx.mk_subsingleton_instance(type);
@@ -472,8 +480,7 @@ void congruence_closure::apply_simple_eqvs(expr const & e) {
         expr const & cast = get_app_args(e, args);
         expr const & a    = args[3];
         expr proof        = mk_app(mk_constant(get_cast_heq_name(), const_levels(cast)), args);
-        bool heq_proof    = true;
-        push_todo(e, a, proof, heq_proof);
+        push_heq(e, a, proof);
     }
 
     if (is_app_of(e, get_eq_rec_name(), 6)) {
@@ -488,13 +495,14 @@ void congruence_closure::apply_simple_eqvs(expr const & e) {
         level l_2  = head(const_levels(eq_rec));
         level l_1  = head(tail(const_levels(eq_rec)));
         expr proof = mk_app({mk_constant(get_eq_rec_heq_name(), {l_1, l_2}), A, P, a, a_prime, H, p});
-        bool heq_proof = true;
-        push_todo(e, p, proof, heq_proof);
+        push_heq(e, p, proof);
     }
 
     if (auto r = m_ctx.reduce_projection(e)) {
         push_refl_eq(e, *r);
     }
+
+    propagate_up(e);
 }
 
 void congruence_closure::add_occurrence(expr const & parent, expr const & child, bool symm_table) {
@@ -545,8 +553,7 @@ void congruence_closure::check_eq_true(symm_congr_key const & k) {
     rhs = get_root(rhs);
     if (lhs != rhs) return;
     // Add e = true
-    bool heq_proof = false;
-    push_todo(e, mk_true(), *g_eq_true_mark, heq_proof);
+    push_eq(e, mk_true(), *g_eq_true_mark);
 }
 
 void congruence_closure::add_symm_congruence_table(expr const & e) {
@@ -561,8 +568,7 @@ void congruence_closure::add_symm_congruence_table(expr const & e) {
         new_entry.m_cg_root = old_k->m_expr;
         m_state.m_entries.insert(e, new_entry);
         /* 2. Put new equivalence in the TODO queue */
-        bool heq_proof      = false;
-        push_todo(e, old_k->m_expr, *g_congr_mark, heq_proof);
+        push_eq(e, old_k->m_expr, *g_congr_mark);
     } else {
         m_state.m_symm_congruences.insert(k);
     }
@@ -594,6 +600,7 @@ void congruence_closure::state::mk_entry_core(expr const & e, bool interpreted,
 }
 
 void congruence_closure::mk_entry(expr const & e, bool interpreted) {
+    if (get_entry(e)) return;
     bool constructor = static_cast<bool>(is_constructor_app(env(), e));
     m_state.mk_entry_core(e, interpreted, constructor);
     process_subsingleton_elem(e);
@@ -777,6 +784,10 @@ void congruence_closure::internalize_core(expr const & e, optional<expr> const &
             if (is_arrow(e) && m_ctx.is_prop(binding_domain(e)) && m_ctx.is_prop(binding_body(e))) {
                 internalize_core(binding_domain(e), some_expr(e));
                 internalize_core(binding_body(e), some_expr(e));
+                bool symm_table = false;
+                add_occurrence(e, binding_domain(e), symm_table);
+                add_occurrence(e, binding_body(e), symm_table);
+                propagate_imp_up(e);
             }
             if (m_ctx.is_prop(e)) {
                 mk_entry(e, false);
@@ -823,17 +834,22 @@ void congruence_closure::invert_trans(expr const & e) {
     invert_trans(e, false, none_expr(), none_expr());
 }
 
-void congruence_closure::remove_parents(expr const & e) {
+void congruence_closure::remove_parents(expr const & e, buffer<expr> & parents_to_propagate) {
     auto ps = m_state.m_parents.find(e);
     if (!ps) return;
-    ps->for_each([&](parent_occ const & p) {
-            lean_trace(name({"debug", "cc"}), scope_trace_env(m_ctx.env(), m_ctx); tout() << "remove parent: " << p.m_expr << "\n";);
-            if (p.m_symm_table) {
-                symm_congr_key k = mk_symm_congr_key(p.m_expr);
-                m_state.m_symm_congruences.erase(k);
-            } else {
-                congr_key k = mk_congr_key(p.m_expr);
-                m_state.m_congruences.erase(k);
+    ps->for_each([&](parent_occ const & pocc) {
+            expr const & p = pocc.m_expr;
+            lean_trace(name({"debug", "cc"}), scope_trace_env(m_ctx.env(), m_ctx); tout() << "remove parent: " << p << "\n";);
+            if (may_propagate(p))
+                parents_to_propagate.push_back(p);
+            if (is_app(p)) {
+                if (pocc.m_symm_table) {
+                    symm_congr_key k = mk_symm_congr_key(p);
+                    m_state.m_symm_congruences.erase(k);
+                } else {
+                    congr_key k = mk_congr_key(p);
+                    m_state.m_congruences.erase(k);
+                }
             }
         });
 }
@@ -843,10 +859,12 @@ void congruence_closure::reinsert_parents(expr const & e) {
     if (!ps) return;
     ps->for_each([&](parent_occ const & p) {
             lean_trace(name({"debug", "cc"}), scope_trace_env(m_ctx.env(), m_ctx); tout() << "reinsert parent: " << p.m_expr << "\n";);
-            if (p.m_symm_table) {
-                add_symm_congruence_table(p.m_expr);
-            } else {
-                add_congruence_table(p.m_expr);
+            if (is_app(p.m_expr)) {
+                if (p.m_symm_table) {
+                    add_symm_congruence_table(p.m_expr);
+                } else {
+                    add_congruence_table(p.m_expr);
+                }
             }
         });
 }
@@ -1173,14 +1191,12 @@ void congruence_closure::push_subsingleton_eq(expr const & a, expr const & b) {
     /* TODO(Leo): check if the following test is a performance bottleneck */
     if (m_ctx.relaxed_is_def_eq(A, B)) {
         /* TODO(Leo): to improve performance we can create the following proof lazily */
-        bool heq_proof = false;
         expr proof     = mk_app(m_ctx, get_subsingleton_elim_name(), a, b);
-        push_todo(a, b, proof, heq_proof);
+        push_eq(a, b, proof);
     } else {
         expr A_eq_B    = *get_eq_proof(A, B);
         expr proof     = mk_app(m_ctx, get_subsingleton_helim_name(), A_eq_B, a, b);
-        bool heq_proof = true;
-        push_todo(a, b, proof, heq_proof);
+        push_heq(a, b, proof);
     }
 }
 
@@ -1213,19 +1229,18 @@ void congruence_closure::propagate_constructor_eq(expr const & e1, expr const &
     lean_assert(c1 && c2);
     expr type       = mk_eq(m_ctx, e1, e2);
     expr h          = *get_eq_proof(e1, e2);
-    bool heq_proof  = false;
     if (*c1 == *c2) {
         buffer<std::tuple<expr, expr, expr>> implied_eqs;
         mk_constructor_eq_constructor_implied_eqs(m_ctx, e1, e2, h, implied_eqs);
         for (std::tuple<expr, expr, expr> const & t : implied_eqs) {
             expr lhs, rhs, H;
             std::tie(lhs, rhs, H) = t;
-            push_todo(lhs, rhs, H, heq_proof);
+            push_eq(lhs, rhs, H);
         }
     } else {
         if (optional<expr> false_pr = mk_constructor_eq_constructor_inconsistency_proof(m_ctx, e1, e2, h)) {
             expr H        = mk_app(mk_constant(get_true_eq_false_of_false_name()), *false_pr);
-            push_todo(mk_true(), mk_false(), H, heq_proof);
+            push_eq(mk_true(), mk_false(), H);
         }
     }
 }
@@ -1254,6 +1269,255 @@ void congruence_closure::propagate_projection_constructor(expr const & p, expr c
     internalize_core(new_p, none_expr());
 }
 
+bool congruence_closure::is_eq_true(expr const & e) const {
+    return is_eqv(e, mk_true());
+}
+
+bool congruence_closure::is_eq_false(expr const & e) const {
+    return is_eqv(e, mk_false());
+}
+
+// Remark: possible optimization: use delayed proof macros for get_eq_true_proof, get_eq_false_proof and get_prop_eq_proof
+
+expr congruence_closure::get_eq_true_proof(expr const & e) const {
+    lean_assert(is_eq_true(e));
+    return *get_eq_proof(e, mk_true());
+}
+
+expr congruence_closure::get_eq_false_proof(expr const & e) const {
+    lean_assert(is_eq_false(e));
+    return *get_eq_proof(e, mk_false());
+}
+
+expr congruence_closure::get_prop_eq_proof(expr const & a, expr const & b) const {
+    lean_assert(is_eqv(a, b));
+    return *get_eq_proof(a, b);
+}
+
+static expr * g_iff_eq_of_eq_true_left  = nullptr;
+static expr * g_iff_eq_of_eq_true_right = nullptr;
+static expr * g_iff_eq_true_of_eq       = nullptr;
+
+void congruence_closure::propagate_iff_up(expr const & e) {
+    expr a, b;
+    lean_verify(is_iff(e, a, b));
+
+    if (is_eq_true(a)) {
+        // a = true  -> (iff a b) = b
+        push_eq(e, b, mk_app(*g_iff_eq_of_eq_true_left, a, b, get_eq_true_proof(a)));
+    } else if (is_eq_true(b)) {
+        // b = true  -> (iff a b) = a
+        push_eq(e, a, mk_app(*g_iff_eq_of_eq_true_right, a, b, get_eq_true_proof(b)));
+    } else if (is_eqv(a, b)) {
+        // a = b     -> (iff a b) = true
+        push_eq(e, mk_true(), mk_app(*g_iff_eq_true_of_eq, a, b, get_prop_eq_proof(a, b)));
+    }
+}
+
+static expr * g_and_eq_of_eq_true_left   = nullptr;
+static expr * g_and_eq_of_eq_true_right  = nullptr;
+static expr * g_and_eq_of_eq_false_left  = nullptr;
+static expr * g_and_eq_of_eq_false_right = nullptr;
+static expr * g_and_eq_of_eq             = nullptr;
+
+void congruence_closure::propagate_and_up(expr const & e) {
+    expr a, b;
+    lean_verify(is_and(e, a, b));
+
+    if (is_eq_true(a)) {
+        // a = true  -> (and a b) = b
+        push_eq(e, b, mk_app(*g_and_eq_of_eq_true_left, a, b, get_eq_true_proof(a)));
+    } else if (is_eq_true(b)) {
+        // b = true  -> (and a b) = a
+        push_eq(e, a, mk_app(*g_and_eq_of_eq_true_right, a, b, get_eq_true_proof(b)));
+    } else if (is_eq_false(a)) {
+        // a = false -> (and a b) = false
+        push_eq(e, mk_false(), mk_app(*g_and_eq_of_eq_false_left, a, b, get_eq_false_proof(a)));
+    } else if (is_eq_false(b)) {
+        // b = false -> (and a b) = false
+        push_eq(e, mk_false(), mk_app(*g_and_eq_of_eq_false_right, a, b, get_eq_false_proof(b)));
+    } else if (is_eqv(a, b)) {
+        // a = b     -> (and a b) = a
+        push_eq(e, a, mk_app(*g_and_eq_of_eq, a, b, get_prop_eq_proof(a, b)));
+    }
+
+    // We may also add
+    // a = not b -> (and a b) = false
+}
+
+static expr * g_or_eq_of_eq_true_left   = nullptr;
+static expr * g_or_eq_of_eq_true_right  = nullptr;
+static expr * g_or_eq_of_eq_false_left  = nullptr;
+static expr * g_or_eq_of_eq_false_right = nullptr;
+static expr * g_or_eq_of_eq             = nullptr;
+
+void congruence_closure::propagate_or_up(expr const & e) {
+    expr a, b;
+    lean_verify(is_or(e, a, b));
+
+    if (is_eq_true(a)) {
+        // a = true  -> (or a b) = true
+        push_eq(e, mk_true(), mk_app(*g_or_eq_of_eq_true_left, a, b, get_eq_true_proof(a)));
+    } else if (is_eq_true(b)) {
+        // b = true  -> (or a b) = true
+        push_eq(e, mk_true(), mk_app(*g_or_eq_of_eq_true_right, a, b, get_eq_true_proof(b)));
+    } else if (is_eq_false(a)) {
+        // a = false -> (or a b) = b
+        push_eq(e, b, mk_app(*g_or_eq_of_eq_false_left, a, b, get_eq_false_proof(a)));
+    } else if (is_eq_false(b)) {
+        // b = false -> (or a b) = a
+        push_eq(e, a, mk_app(*g_or_eq_of_eq_false_right, a, b, get_eq_false_proof(b)));
+    } else if (is_eqv(a, b)) {
+        // a = b     -> (or a b) = a
+        push_eq(e, a, mk_app(*g_or_eq_of_eq, a, b, get_prop_eq_proof(a, b)));
+    }
+
+    // We may also add
+    // a = not b -> (or a b) = true
+}
+
+static expr * g_not_eq_of_eq_true   = nullptr;
+static expr * g_not_eq_of_eq_false  = nullptr;
+static expr * g_false_of_a_eq_not_a = nullptr;
+
+void congruence_closure::propagate_not_up(expr const & e) {
+    expr a;
+    lean_verify(is_not(e, a));
+
+    if (is_eq_true(a)) {
+        // a = true  -> not a = false
+        push_eq(e, mk_false(), mk_app(*g_not_eq_of_eq_true, a, get_eq_true_proof(a)));
+    } else if (is_eq_false(a)) {
+        // a = false -> not a = true
+        push_eq(e, mk_true(), mk_app(*g_not_eq_of_eq_false, a, get_eq_false_proof(a)));
+    } else if (is_eqv(a, e)) {
+        expr false_pr = mk_app(*g_false_of_a_eq_not_a, a, get_prop_eq_proof(a, e));
+        expr H        = mk_app(mk_constant(get_true_eq_false_of_false_name()), false_pr);
+        push_eq(mk_true(), mk_false(), H);
+    }
+}
+
+static expr * g_imp_eq_of_eq_true_left  = nullptr;
+static expr * g_imp_eq_of_eq_false_left = nullptr;
+static expr * g_imp_eq_of_eq_true_right = nullptr;
+static expr * g_imp_eq_true_of_eq       = nullptr;
+
+void congruence_closure::propagate_imp_up(expr const & e) {
+    lean_assert(is_arrow(e));
+    expr a = binding_domain(e);
+    expr b = binding_body(e);
+
+    if (is_eq_true(a)) {
+        // a = true  -> (a -> b) = b
+        push_eq(e, b, mk_app(*g_imp_eq_of_eq_true_left, a, b, get_eq_true_proof(a)));
+    } else if (is_eq_false(a)) {
+        // a = false -> (a -> b) = true
+        push_eq(e, mk_true(), mk_app(*g_imp_eq_of_eq_false_left, a, b, get_eq_false_proof(a)));
+    } else if (is_eq_true(b)) {
+        // b = true  -> (a -> b) = true
+        push_eq(e, mk_true(), mk_app(*g_imp_eq_of_eq_true_right, a, b, get_eq_true_proof(b)));
+    } else if (is_eqv(a, b)) {
+        // a = b     -> (a -> b) = true
+        push_eq(e, mk_true(), mk_app(*g_imp_eq_true_of_eq, a, b, get_prop_eq_proof(a, b)));
+    }
+}
+
+static name * g_if_eq_of_eq_true  = nullptr;
+static name * g_if_eq_of_eq_false = nullptr;
+static name * g_if_eq_of_eq       = nullptr;
+
+void congruence_closure::propagate_ite_up(expr const & e) {
+    expr c, d, A, a, b;
+    lean_verify(is_ite(e, c, d, A, a, b));
+
+    if (is_eq_true(c)) {
+        // c = true  -> (ite c a b) = a
+        level lvl = get_level(m_ctx, A);
+        push_eq(e, a, mk_app({mk_constant(*g_if_eq_of_eq_true, {lvl}), c, d, A, a, b, get_eq_true_proof(c)}));
+    } else if (is_eq_false(c)) {
+        // c = false -> (ite c a b) = b
+        level lvl = get_level(m_ctx, A);
+        push_eq(e, b, mk_app({mk_constant(*g_if_eq_of_eq_false, {lvl}), c, d, A, a, b, get_eq_false_proof(c)}));
+    } else if (is_eqv(a, b)) {
+        // a = b     -> (ite c a b) = a
+        level lvl = get_level(m_ctx, A);
+        push_eq(e, a, mk_app({mk_constant(*g_if_eq_of_eq, {lvl}), c, d, A, a, b, get_prop_eq_proof(a, b)}));
+    }
+}
+
+bool congruence_closure::may_propagate(expr const & e) {
+    return
+        is_iff(e) || is_and(e) || is_or(e) || is_not(e) || is_arrow(e) || is_ite(e);
+}
+
+void congruence_closure::propagate_up(expr const & e) {
+    if (m_state.m_inconsistent) return;
+    if (is_iff(e)) {
+        propagate_iff_up(e);
+    } else if (is_and(e)) {
+        propagate_and_up(e);
+    } else if (is_or(e)) {
+        propagate_or_up(e);
+    } else if (is_not(e)) {
+        propagate_not_up(e);
+    } else if (is_arrow(e)) {
+        propagate_imp_up(e);
+    } else if (is_ite(e)) {
+        propagate_ite_up(e);
+    }
+}
+
+static expr * g_eq_true_of_and_eq_true_left  = nullptr;
+static expr * g_eq_true_of_and_eq_true_right = nullptr;
+
+void congruence_closure::propagate_and_down(expr const & e) {
+    if (is_eq_true(e)) {
+        expr a, b;
+        lean_verify(is_and(e, a, b));
+        expr h = get_eq_true_proof(e);
+        push_eq(a, mk_true(), mk_app(*g_eq_true_of_and_eq_true_left, a, b, h));
+        push_eq(b, mk_true(), mk_app(*g_eq_true_of_and_eq_true_right, a, b, h));
+    }
+}
+
+static expr * g_eq_false_of_or_eq_false_left  = nullptr;
+static expr * g_eq_false_of_or_eq_false_right = nullptr;
+
+void congruence_closure::propagate_or_down(expr const & e) {
+    if (is_eq_false(e)) {
+        expr a, b;
+        lean_verify(is_or(e, a, b));
+        expr h = get_eq_false_proof(e);
+        push_eq(a, mk_false(), mk_app(*g_eq_false_of_or_eq_false_left, a, b, h));
+        push_eq(b, mk_false(), mk_app(*g_eq_false_of_or_eq_false_right, a, b, h));
+    }
+}
+
+static expr * g_eq_false_of_not_eq_true = nullptr;
+static expr * g_eq_true_of_not_eq_false = nullptr;
+
+void congruence_closure::propagate_not_down(expr const & e) {
+    if (is_eq_true(e)) {
+        expr a;
+        lean_verify(is_not(e, a));
+        push_eq(a, mk_false(), mk_app(*g_eq_false_of_not_eq_true, a, get_eq_true_proof(e)));
+    } else if (m_state.m_config.m_em && is_eq_false(e)) {
+        expr a;
+        lean_verify(is_not(e, a));
+        push_eq(a, mk_true(), mk_app(*g_eq_true_of_not_eq_false, a, get_eq_false_proof(e)));
+    }
+}
+
+void congruence_closure::propagate_down(expr const & e) {
+    if (is_and(e)) {
+        propagate_and_down(e);
+    } else if (is_or(e)) {
+        propagate_or_down(e);
+    } else if (is_not(e)) {
+        propagate_not_down(e);
+    }
+}
+
 void congruence_closure::propagate_value_inconsistency(expr const & e1, expr const & e2) {
     lean_assert(is_interpreted_value(e1));
     lean_assert(is_interpreted_value(e2));
@@ -1261,8 +1525,7 @@ void congruence_closure::propagate_value_inconsistency(expr const & e1, expr con
     expr eq_proof      = *get_eq_proof(e1, e2);
     expr true_eq_false = mk_eq(m_ctx, mk_true(), mk_false());
     expr H             = mk_absurd(m_ctx, eq_proof, ne_proof, true_eq_false);
-    bool heq_proof     = false;
-    push_todo(mk_true(), mk_false(), H, heq_proof);
+    push_eq(mk_true(), mk_false(), H);
 }
 
 static bool is_true_or_false(expr const & e) {
@@ -1337,8 +1600,9 @@ void congruence_closure::add_eqv_step(expr e1, expr e2, expr const & H,
     new_n1.m_flipped = flipped;
     m_state.m_entries.insert(e1, new_n1);
 
+    buffer<expr> parents_to_propagate;
     /* The hash code for the parents is going to change */
-    remove_parents(e1_root);
+    remove_parents(e1_root, parents_to_propagate);
 
     /* force all m_root fields in e1 equivalence class to point to e2_root */
     bool propagate = is_true_or_false(e2_root);
@@ -1384,7 +1648,7 @@ void congruence_closure::add_eqv_step(expr e1, expr e2, expr const & H,
         if (auto it = m_state.m_parents.find(e2_root))
             ps2 = *it;
         ps1->for_each([&](parent_occ const & p) {
-                if (is_congr_root(p.m_expr)) {
+                if (is_app(p.m_expr) && is_congr_root(p.m_expr)) {
                     if (!constructor_eq && r2->m_constructor)  {
                         propagate_projection_constructor(p.m_expr, e2_root);
                     }
@@ -1395,25 +1659,32 @@ void congruence_closure::add_eqv_step(expr e1, expr e2, expr const & H,
         m_state.m_parents.insert(e2_root, ps2);
     }
 
+    if (!m_state.m_inconsistent && ac_var1 && ac_var2)
+        m_ac.add_eq(*ac_var1, *ac_var2);
+
+    if (!m_state.m_inconsistent && constructor_eq)
+        propagate_constructor_eq(e1_root, e2_root);
+
+    if (!m_state.m_inconsistent && value_inconsistency)
+        propagate_value_inconsistency(e1_root, e2_root);
+
     if (!m_state.m_inconsistent) {
-        if (ac_var1 && ac_var2)
-            m_ac.add_eq(*ac_var1, *ac_var2);
-
-        if (constructor_eq) {
-            propagate_constructor_eq(e1_root, e2_root);
-        }
-
-        if (value_inconsistency) {
-            propagate_value_inconsistency(e1_root, e2_root);
-        }
-
         update_mt(e2_root);
         check_new_subsingleton_eq(e1_root, e2_root);
-
-        if (!to_propagate.empty() && m_phandler) {
-            m_phandler->propagated(to_propagate);
-        }
     }
+
+    if (!m_state.m_inconsistent) {
+        for (expr const & p : parents_to_propagate)
+            propagate_up(p);
+    }
+
+    if (!m_state.m_inconsistent && !to_propagate.empty()) {
+        for (expr const & e : to_propagate)
+            propagate_down(e);
+        if (m_phandler)
+            m_phandler->propagated(to_propagate);
+    }
+
     lean_trace(name({"cc", "merge"}), scope_trace_env scope(m_ctx.env(), m_ctx);
                tout() << e1_root << " = " << e2_root << "\n";);
     lean_trace(name({"debug", "cc"}), scope_trace_env scope(m_ctx.env(), m_ctx);
@@ -1626,11 +1897,87 @@ void initialize_congruence_closure() {
     g_congr_mark    = new expr(mk_constant(name(prefix, "[congruence]")));
     g_eq_true_mark  = new expr(mk_constant(name(prefix, "[iff-true]")));
     g_refl_mark     = new expr(mk_constant(name(prefix, "[refl]")));
+
+    g_iff_eq_of_eq_true_left  = new expr(mk_constant("iff_eq_of_eq_true_left"));
+    g_iff_eq_of_eq_true_right = new expr(mk_constant("iff_eq_of_eq_true_right"));
+    g_iff_eq_true_of_eq       = new expr(mk_constant("iff_eq_true_of_eq"));
+
+    g_and_eq_of_eq_true_left   = new expr(mk_constant("and_eq_of_eq_true_left"));
+    g_and_eq_of_eq_true_right  = new expr(mk_constant("and_eq_of_eq_true_right"));
+    g_and_eq_of_eq_false_left  = new expr(mk_constant("and_eq_of_eq_false_left"));
+    g_and_eq_of_eq_false_right = new expr(mk_constant("and_eq_of_eq_false_right"));
+    g_and_eq_of_eq             = new expr(mk_constant("and_eq_of_eq"));
+
+    g_or_eq_of_eq_true_left   = new expr(mk_constant("or_eq_of_eq_true_left"));
+    g_or_eq_of_eq_true_right  = new expr(mk_constant("or_eq_of_eq_true_right"));
+    g_or_eq_of_eq_false_left  = new expr(mk_constant("or_eq_of_eq_false_left"));
+    g_or_eq_of_eq_false_right = new expr(mk_constant("or_eq_of_eq_false_right"));
+    g_or_eq_of_eq             = new expr(mk_constant("or_eq_of_eq"));
+
+    g_not_eq_of_eq_true       = new expr(mk_constant("not_eq_of_eq_true "));
+    g_not_eq_of_eq_false      = new expr(mk_constant("not_eq_of_eq_false"));
+    g_false_of_a_eq_not_a     = new expr(mk_constant("false_of_a_eq_not_a"));
+
+    g_imp_eq_of_eq_true_left  = new expr(mk_constant("imp_eq_of_eq_true_left"));
+    g_imp_eq_of_eq_false_left = new expr(mk_constant("imp_eq_of_eq_false_left"));
+    g_imp_eq_of_eq_true_right = new expr(mk_constant("imp_eq_of_eq_true_right"));
+    g_imp_eq_true_of_eq       = new expr(mk_constant("imp_eq_true_of_eq"));
+
+    g_if_eq_of_eq_true  = new name("if_eq_of_eq_true");
+    g_if_eq_of_eq_false = new name("if_eq_of_eq_false");
+    g_if_eq_of_eq       = new name("if_eq_of_eq");
+
+    g_eq_true_of_and_eq_true_left  = new expr(mk_constant("eq_true_of_and_eq_true_left"));
+    g_eq_true_of_and_eq_true_right = new expr(mk_constant("eq_true_of_and_eq_true_right"));
+
+    g_eq_false_of_or_eq_false_left  = new expr(mk_constant("eq_false_of_or_eq_false_left"));
+    g_eq_false_of_or_eq_false_right = new expr(mk_constant("eq_false_of_or_eq_false_right"));
+
+    g_eq_false_of_not_eq_true = new expr(mk_constant("eq_false_of_not_eq_true"));
+    g_eq_true_of_not_eq_false = new expr(mk_constant("eq_true_of_not_eq_false"));
 }
 
 void finalize_congruence_closure() {
     delete g_congr_mark;
     delete g_eq_true_mark;
     delete g_refl_mark;
+
+    delete g_iff_eq_of_eq_true_left;
+    delete g_iff_eq_of_eq_true_right;
+    delete g_iff_eq_true_of_eq;
+
+    delete g_and_eq_of_eq_true_left;
+    delete g_and_eq_of_eq_true_right;
+    delete g_and_eq_of_eq_false_left;
+    delete g_and_eq_of_eq_false_right;
+    delete g_and_eq_of_eq;
+
+    delete g_or_eq_of_eq_true_left;
+    delete g_or_eq_of_eq_true_right;
+    delete g_or_eq_of_eq_false_left;
+    delete g_or_eq_of_eq_false_right;
+    delete g_or_eq_of_eq;
+
+    delete g_not_eq_of_eq_true;
+    delete g_not_eq_of_eq_false;
+    delete g_false_of_a_eq_not_a;
+
+    delete g_imp_eq_of_eq_true_left;
+    delete g_imp_eq_of_eq_false_left;
+    delete g_imp_eq_of_eq_true_right;
+    delete g_imp_eq_true_of_eq;
+
+    delete g_if_eq_of_eq_true;
+    delete g_if_eq_of_eq_false;
+    delete g_if_eq_of_eq;
+
+    delete g_eq_true_of_and_eq_true_left;
+    delete g_eq_true_of_and_eq_true_right;
+
+    delete g_eq_false_of_or_eq_false_left;
+    delete g_eq_false_of_or_eq_false_right;
+
+    delete g_eq_false_of_not_eq_true;
+    delete g_eq_true_of_not_eq_false;
 }
 }
diff --git a/src/library/tactic/smt/congruence_closure.h b/src/library/tactic/smt/congruence_closure.h
index f4b5a1a201..1233e02bbf 100644
--- a/src/library/tactic/smt/congruence_closure.h
+++ b/src/library/tactic/smt/congruence_closure.h
@@ -109,7 +109,8 @@ public:
         unsigned m_values:1;
         unsigned m_all_ho:1;
         unsigned m_ac:1;
-        config() { m_ignore_instances = true; m_values = true; m_all_ho = false; m_ac = true; }
+        unsigned m_em:1;
+        config() { m_ignore_instances = true; m_values = true; m_all_ho = false; m_ac = true; m_em = true; }
     };
 
     class state {
@@ -197,11 +198,12 @@ private:
     void internalize_app(expr const & e);
     void internalize_core(expr const & e, optional<expr> const & parent);
     void push_todo(expr const & lhs, expr const & rhs, expr const & H, bool heq_proof);
-    void push_new_eq(expr const & lhs, expr const & rhs, expr const & H) { push_todo(lhs, rhs, H, false); }
+    void push_heq(expr const & lhs, expr const & rhs, expr const & H);
+    void push_eq(expr const & lhs, expr const & rhs, expr const & H);
     void push_refl_eq(expr const & lhs, expr const & rhs);
     void invert_trans(expr const & e, bool new_flipped, optional<expr> new_target, optional<expr> new_proof);
     void invert_trans(expr const & e);
-    void remove_parents(expr const & e);
+    void remove_parents(expr const & e, buffer<expr> & parents_to_propagate);
     void reinsert_parents(expr const & e);
     void update_mt(expr const & e);
     bool has_heq_proofs(expr const & root) const;
@@ -217,6 +219,23 @@ private:
     optional<expr> get_eq_proof_core(expr const & e1, expr const & e2, bool as_heq) const;
     void push_subsingleton_eq(expr const & a, expr const & b);
     void check_new_subsingleton_eq(expr const & old_root, expr const & new_root);
+    bool is_eq_true(expr const & e) const;
+    bool is_eq_false(expr const & e) const;
+    expr get_eq_true_proof(expr const & e) const;
+    expr get_eq_false_proof(expr const & e) const;
+    expr get_prop_eq_proof(expr const & a, expr const & b) const;
+    static bool may_propagate(expr const & e);
+    void propagate_iff_up(expr const & e);
+    void propagate_and_up(expr const & e);
+    void propagate_or_up(expr const & e);
+    void propagate_not_up(expr const & e);
+    void propagate_imp_up(expr const & e);
+    void propagate_ite_up(expr const & e);
+    void propagate_up(expr const & e);
+    void propagate_and_down(expr const & e);
+    void propagate_or_down(expr const & e);
+    void propagate_not_down(expr const & e);
+    void propagate_down(expr const & e);
     void propagate_inst_implicit(expr const & e);
     void propagate_constructor_eq(expr const & e1, expr const & e2);
     void propagate_projection_constructor(expr const & p, expr const & c);
diff --git a/src/library/tactic/smt/congruence_tactics.cpp b/src/library/tactic/smt/congruence_tactics.cpp
index 3129d0cecc..19a3d8658e 100644
--- a/src/library/tactic/smt/congruence_tactics.cpp
+++ b/src/library/tactic/smt/congruence_tactics.cpp
@@ -51,6 +51,7 @@ structure cc_config :=
 (ignore_instances : bool)
 (ac               : bool)
 (ho_fns           : option (list name))
+(em               : bool)
 */
 pair<name_set, congruence_closure::config> to_ho_fns_cc_config(vm_obj const & cfg) {
     congruence_closure::config c;
@@ -63,6 +64,7 @@ pair<name_set, congruence_closure::config> to_ho_fns_cc_config(vm_obj const & cf
         c.m_all_ho       = false;
         ho_fns           = to_name_set(to_list_name(get_some_value(cfield(cfg, 2))));
     }
+    c.m_em               = to_bool(cfield(cfg, 3));
     return mk_pair(ho_fns, c);
 }
 
diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp
index aa1eff3208..6eebb85377 100644
--- a/src/library/tactic/smt/smt_state.cpp
+++ b/src/library/tactic/smt/smt_state.cpp
@@ -33,8 +33,7 @@ smt_goal::smt_goal(smt_config const & cfg):
 smt::smt(type_context & ctx, smt_goal & g):
     m_ctx(ctx),
     m_goal(g),
-    m_cc(ctx, m_goal.m_cc_state, this),
-    m_up(ctx, m_goal.m_up_state, *this) {
+    m_cc(ctx, m_goal.m_cc_state, this) {
 }
 
 smt::~smt() {
@@ -47,9 +46,6 @@ void smt::propagated(unsigned n, expr const * p) {
                format r;
                for (unsigned i = 0; i < n; i++) { if (i > 0) r += comma() + line(); r += fmt(p[i]); }
                tout() << group(format("new facts:") + line() + bracket("{", r, "}")) << "\n";);
-    for (unsigned i = 0; i < n; i++) {
-        m_up.assigned(p[i]);
-    }
 }
 
 lbool smt::get_value_core(expr const & e) {
diff --git a/src/library/tactic/smt/smt_state.h b/src/library/tactic/smt/smt_state.h
index 73245d0fce..981b2849c0 100644
--- a/src/library/tactic/smt/smt_state.h
+++ b/src/library/tactic/smt/smt_state.h
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 #include "library/discr_tree.h"
 #include "library/tactic/simp_lemmas.h"
-#include "library/tactic/smt/unit_propagation.h"
 #include "library/tactic/smt/congruence_closure.h"
 #include "library/tactic/smt/ematch.h"
 
@@ -25,7 +24,6 @@ class smt_goal {
     friend class smt;
     cc_state          m_cc_state;
     ematch_state      m_em_state;
-    up_state          m_up_state;
     simp_lemmas       m_simp_lemmas;
 public:
     smt_goal(smt_config const & cfg);
@@ -33,16 +31,16 @@ public:
     simp_lemmas const & get_simp_lemmas() const { return m_simp_lemmas; }
 };
 
-class smt : public cc_propagation_handler, public up_assignment {
+class smt : public cc_propagation_handler {
 private:
     type_context &     m_ctx;
     smt_goal &         m_goal;
     congruence_closure m_cc;
-    unit_propagation   m_up;
 
     lbool get_value_core(expr const & e);
+    lbool get_value(expr const & e);
     virtual void propagated(unsigned n, expr const * p) override;
-    virtual lbool get_value(expr const & e) override;
+
 public:
     smt(type_context & ctx, smt_goal & g);
     virtual ~smt();
@@ -50,7 +48,7 @@ public:
     void internalize(expr const & e);
     void add(expr const & type, expr const & proof);
 
-    virtual optional<expr> get_proof(expr const & e) override;
+    optional<expr> get_proof(expr const & e);
     bool inconsistent() const { return m_cc.inconsistent(); }
     optional<expr> get_inconsistency_proof() const { return m_cc.get_inconsistency_proof(); }
     optional<expr> get_eq_proof(expr const & lhs, expr const & rhs) const {
diff --git a/src/library/tactic/smt/theory_ac.cpp b/src/library/tactic/smt/theory_ac.cpp
index 32e407298f..62bac7fa61 100644
--- a/src/library/tactic/smt/theory_ac.cpp
+++ b/src/library/tactic/smt/theory_ac.cpp
@@ -478,7 +478,7 @@ void theory_ac::process() {
 
         /* Propagate new equality to congruence closure module */
         if (!is_ac_app(lhs) && !is_ac_app(rhs) && m_cc.get_root(lhs) != m_cc.get_root(rhs)) {
-            m_cc.push_new_eq(lhs, rhs, mark_cc_theory_proof(H));
+            m_cc.push_eq(lhs, rhs, mark_cc_theory_proof(H));
         }
 
         /* Orient */
diff --git a/src/library/tactic/smt/unit_propagation.cpp b/src/library/tactic/smt/unit_propagation.cpp
deleted file mode 100644
index f7c2b3b8c6..0000000000
--- a/src/library/tactic/smt/unit_propagation.cpp
+++ /dev/null
@@ -1,125 +0,0 @@
-/*
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "library/util.h"
-#include "library/trace.h"
-#include "library/tactic/smt/unit_propagation.h"
-
-namespace lean {
-static bool is_lemma(type_context & ctx, expr e) {
-    if (!ctx.is_prop(e)) return false;
-    bool arrow = false;
-    while (is_arrow(e) && !is_not(e)) {
-        arrow = true;
-        if (!ctx.is_prop(binding_domain(e))) return false;
-        e     = binding_body(e);
-    }
-    return arrow || is_or(e);
-}
-
-/** \brief e is a dependent lemma when
-    - e is a proposition
-    - e is of the form (Pi (x : A), B)
-    - A is a proposition
-    - B depends on x */
-static bool is_dep_lemma(type_context & ctx, expr const & e) {
-    return
-        is_pi(e) &&
-        ctx.is_prop(e) &&
-        ctx.is_prop(binding_domain(e)) &&
-        !closed(binding_body(e));
-}
-
-static bool is_fact(type_context & ctx, expr const & e) {
-    return ctx.is_prop(e) && !is_lemma(ctx, e) && !is_dep_lemma(ctx, e);
-}
-
-unit_propagation::unit_propagation(type_context & ctx, state & s, assignment & assignment):
-    m_ctx(ctx), m_state(s), m_assignment(assignment) {}
-
-static expr get_var(expr const & e) {
-    expr arg;
-    if (is_not(e, arg))
-        return arg;
-    else
-        return e;
-}
-
-void unit_propagation::visit_lemma(expr const & e) {
-    lean_assert(is_lemma(ctx, e));
-    expr it        = e;
-    unsigned i     = 0;
-    expr watches[2];
-
-    /* Traverse A_i */
-    while (is_arrow(it) && !is_not(it) && i < 2) {
-        expr const & p = binding_domain(it);
-        switch (get_value(p)) {
-        case l_true:   break;
-        case l_false: case l_undef:
-            watches[i] = get_var(p);
-            i++;
-            break;
-        }
-        it = binding_body(it);
-    }
-
-    /* Traverse B_j */
-    bool done = false;
-    while (!done && i < 2) {
-        expr p, next_it;
-        if (is_or(it, p, next_it)) {
-            it   = next_it;
-        } else {
-            p    = it;
-            done = true;
-        }
-        switch (get_value(p)) {
-        case l_false: break;
-        case l_true: case l_undef:
-            watches[i] = get_var(p);
-            i++;
-            break;
-        }
-    }
-
-    if (i == 2) {
-        m_state.m_facts_to_lemmas.insert(watches[0], e);
-        m_state.m_facts_to_lemmas.insert(watches[1], e);
-        return;
-    }
-
-    if (i == 0) return;
-
-    /* TODO(Leo): */
-}
-
-void unit_propagation::visit_dep_lemma(expr const & /* e */) {
-    /* TODO(Leo): */
-}
-
-void unit_propagation::propagate(expr const & e) {
-    if (list<expr> const * lemmas = m_state.m_facts_to_lemmas.find(e)) {
-        for (expr const & lemma : *lemmas)
-            visit_lemma(lemma);
-    }
-
-    if (list<expr> const * lemmas = m_state.m_facts_to_dep_lemmas.find(e)) {
-        for (expr const & lemma : *lemmas)
-            visit_dep_lemma(lemma);
-    }
-}
-
-void unit_propagation::assigned(expr const & e) {
-    if (is_lemma(m_ctx, e) && m_assignment.get_value(e) == l_true) {
-        visit_lemma(e);
-    } else if (is_dep_lemma(m_ctx, e) && m_assignment.get_value(e) == l_true) {
-        visit_dep_lemma(e);
-    } else if (is_fact(m_ctx, e)) {
-        propagate(e);
-    }
-}
-}
diff --git a/src/library/tactic/smt/unit_propagation.h b/src/library/tactic/smt/unit_propagation.h
deleted file mode 100644
index 7d6936c3b5..0000000000
--- a/src/library/tactic/smt/unit_propagation.h
+++ /dev/null
@@ -1,57 +0,0 @@
-/*
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/rb_multi_map.h"
-#include "library/type_context.h"
-
-namespace lean {
-/**
-   The unit propagation module can handle lemmas of the form:
-
-       A_1 -> ... -> A_n -> B_1 \/ ... \/ B_m
-
-   and "propagates" if one of the following conditions hold:
-
-   - We have all A_i, and the negations of all but one B_j.
-   - We have the negations of all B_j, and all but one A_i.
-
-   Each lemma watches two of its facts. */
-class unit_propagation {
-public:
-    class state {
-        friend class unit_propagation;
-        rb_multi_map<expr, expr, expr_quick_cmp> m_facts_to_lemmas;
-        rb_multi_map<expr, expr, expr_quick_cmp> m_facts_to_dep_lemmas;
-    public:
-    };
-
-    class assignment {
-    public:
-        virtual ~assignment() {}
-        virtual lbool get_value(expr const & e) = 0;
-        virtual optional<expr> get_proof(expr const & e) = 0;
-    };
-
-private:
-    type_context & m_ctx;
-    state &        m_state;
-    assignment &   m_assignment;
-
-    lbool get_value(expr const & e) { return m_assignment.get_value(e); }
-    optional<expr> get_proof(expr const & e) { return m_assignment.get_proof(e); }
-    void visit_lemma(expr const & e);
-    void visit_dep_lemma(expr const & e);
-    void propagate(expr const & e);
-
-public:
-    unit_propagation(type_context & ctx, state & s, assignment & assignment);
-    void assigned(expr const & e);
-};
-
-typedef unit_propagation::state up_state;
-typedef unit_propagation::assignment up_assignment;
-}
diff --git a/tests/lean/run/using_smt2.lean b/tests/lean/run/using_smt2.lean
index 7621aef254..d169710a98 100644
--- a/tests/lean/run/using_smt2.lean
+++ b/tests/lean/run/using_smt2.lean
@@ -1,13 +1,40 @@
 open smt_tactic
 
-def ex1 (p q : Prop) : p → q → p :=
+example (p q : Prop) : p → q → p :=
 by using_smt $ return ()
 
-def ex2 (p q : Prop) : ¬ p → q → ¬ p :=
+example (p q : Prop) : ¬ p → q → ¬ p :=
 by using_smt $ return ()
 
-print ex1
-print ex2
-
 example (p q : Prop) : p → (p ↔ q) → q :=
 by using_smt $ return ()
+
+example (p q : Prop) : p → (p → q) → q :=
+by using_smt $ return ()
+
+example (p q : Prop) : (p → q) → p → q :=
+by using_smt $ return ()
+
+example (p q r : Prop) : (p → r → q) → r → p → q :=
+by using_smt $ return ()
+
+example (p q r s t o : Prop) : (p ∨ t → o ∨ r → q ∧ s) → r → p → q :=
+by using_smt $ return ()
+
+example (p q : Prop) (a b c : nat) : (p ∨ q → a = b ∨ a = c) → a ≠ b → p → c = a :=
+by using_smt $ return ()
+
+example (p q : Prop) [decidable p] [decidable q] (a b c : nat) : (if p ∨ q then (a = b ∨ a = c) else (a = 0)) → p → a ≠ b → c = a :=
+by using_smt $ return ()
+
+example (p q : Prop) : p → (p ↔ ¬q) → ¬q :=
+by using_smt $ return ()
+
+example (p q r s : Prop) : (p ∨ q → not (r ∨ s)) → p → not r :=
+by using_smt $ return ()
+
+example (p q r : Prop) (a b c : nat): (p → q ∧ r ∧ a = b + c) → p → (c + b = a ∧ r) :=
+by using_smt $ return ()
+
+example (a b c d : nat) : b = d → c = d → (if a > 10 then b else c) = b :=
+by using_smt $ return ()