diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
index c18c6af13..df2b34ad0 100644
--- a/src/library/blast/simplifier.cpp
+++ b/src/library/blast/simplifier.cpp
@@ -191,6 +191,9 @@ class simplifier {
         simp_rule_sets srss = _srss;
         for (unsigned i = 0; i < ls.size(); i++) {
             expr & l = ls[i];
+            if (m_trace) {
+                ios().get_diagnostic_channel() << "Local: " << l << " : " << mlocal_type(l) << "\n";
+            }
             tmp_type_context tctx(env(), ios());
             srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l);
         }
@@ -593,6 +596,14 @@ result simplifier::rewrite(expr const & e, simp_rule_sets const & srss) {
 result simplifier::rewrite(expr const & e, simp_rule const & sr) {
     blast_tmp_type_context tmp_tctx(sr.get_num_umeta(), sr.get_num_emeta());
 
+    if (m_trace) {
+        expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
+        expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
+        ios().get_diagnostic_channel()
+            << "TRYREW(" << sr.get_id() << ") "
+            << "[" << new_lhs << " =?= " << new_rhs << "]\n";
+    }
+
     if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e);
 
     if (m_trace) {
diff --git a/tests/lean/simplifier11.lean b/tests/lean/simplifier11.lean
index 47e64154b..4f14e25c2 100644
--- a/tests/lean/simplifier11.lean
+++ b/tests/lean/simplifier11.lean
@@ -1,6 +1,10 @@
 -- Conditional congruence
 import logic.connectives logic.quantifiers
 
+-- TODO(dhs): either add this to the library or add a `ceqv` rule for
+-- ¬ c ==> (¬ c ↔ true) in addition to (c ↔ false)
+lemma not_workaround [simp] : ∀ (P : Prop), (P ↔ false) → (¬ P ↔ true) := sorry
+
 namespace if_congr
 constants {A : Type} {b c : Prop} (dec_b : decidable b) (dec_c : decidable c)
           {x y u v : A} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v)