diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp
index 25317e82f..119400cb7 100644
--- a/src/library/simplifier/simplifier.cpp
+++ b/src/library/simplifier/simplifier.cpp
@@ -911,6 +911,12 @@ class simplifier_cell::imp {
                             i   = i + 1;
                         }
                     }
+                    if (new_rhs == target) {
+                        if (m_monitor)
+                            m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(),
+                                                         0, simplifier_monitor::failure_kind::LoopPrevention);
+                        return false;
+                    }
                     if (m_proofs_enabled) {
                         if (num > 0) {
                             new_args[0] = rule.get_proof();
@@ -990,10 +996,10 @@ class simplifier_cell::imp {
                     }
                     new_proof = mk_app(proof_args);
                     new_rhs   = arg(ceq, num_args(ceq) - 1);
-                    if (rule.is_permutation() && !is_lt(new_rhs, target, false)) {
+                    if (new_rhs == target || (rule.is_permutation() && !is_lt(new_rhs, target, false))) {
                         if (m_monitor)
                             m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(),
-                                                         0, simplifier_monitor::failure_kind::PermutationGe);
+                                                         0, simplifier_monitor::failure_kind::LoopPrevention);
                         return false;
                     }
                     if (m_monitor)
@@ -1800,7 +1806,10 @@ static int simplify_core(lua_State * L, ro_shared_environment const & env) {
     options opts;
     if (nargs >= 3)
         opts = to_options(L, 3);
-    auto r = simplify(e, env, opts, rules.size(), rules.data());
+    optional<ro_metavar_env> menv;
+    if (nargs >= 5)
+        menv = some_ro_menv(to_metavar_env(L, 5));
+    auto r = simplify(e, env, opts, rules.size(), rules.data(), menv, get_simplifier_monitor(L, 6));
     push_expr(L, r.get_expr());
     push_optional_expr(L, r.get_proof());
     lua_pushboolean(L, r.is_heq_proof());
@@ -1885,7 +1894,7 @@ void open_simplifier(lua_State * L) {
     SET_ENUM("TypeMismatch",        simplifier_monitor::failure_kind::TypeMismatch);
     SET_ENUM("AssumptionNotProved", simplifier_monitor::failure_kind::AssumptionNotProved);
     SET_ENUM("MissingArgument",     simplifier_monitor::failure_kind::MissingArgument);
-    SET_ENUM("PermutationGe",       simplifier_monitor::failure_kind::PermutationGe);
+    SET_ENUM("LoopPrevention",      simplifier_monitor::failure_kind::LoopPrevention);
     SET_ENUM("AbstractionBody",     simplifier_monitor::failure_kind::AbstractionBody);
     lua_setglobal(L, "simplifier_failure");
 
diff --git a/src/library/simplifier/simplifier.h b/src/library/simplifier/simplifier.h
index a6f83c31e..96455d6d0 100644
--- a/src/library/simplifier/simplifier.h
+++ b/src/library/simplifier/simplifier.h
@@ -102,7 +102,7 @@ public:
     */
     virtual void rewrite_eh(ro_simplifier const & s, expr const & e, expr const & new_e, expr const & ceq, name const & ceq_id) = 0;
 
-    enum class failure_kind { Unsupported, TypeMismatch, AssumptionNotProved, MissingArgument, PermutationGe, AbstractionBody };
+    enum class failure_kind { Unsupported, TypeMismatch, AssumptionNotProved, MissingArgument, LoopPrevention, AbstractionBody };
 
     /**
        \brief This method is invoked when the simplifier fails to rewrite an application \c e.
diff --git a/tests/lean/simp3.lean.expected.out b/tests/lean/simp3.lean.expected.out
index e6e2c7f99..3158f973d 100644
--- a/tests/lean/simp3.lean.expected.out
+++ b/tests/lean/simp3.lean.expected.out
@@ -31,5 +31,5 @@ trans (congr (congr2 (λ x : ℕ, eq ((λ x : ℕ, x + 10) x))
 a * a + (a * b + (b * a + b * b))
 ⊤ → ⊥	refl (⊤ → ⊥)	false
 ⊤ → ⊤	refl (⊤ → ⊤)	false
-⊥ → ⊥	refl (⊥ → ⊥)	false
+⊥ → ⊤	imp_congr (refl ⊥) (λ C::1 : ⊥, eqt_intro C::1)	false
 ⊥	refl ⊥	false
diff --git a/tests/lua/simp1.lua b/tests/lua/simp1.lua
index 16841d36a..fff92f267 100644
--- a/tests/lua/simp1.lua
+++ b/tests/lua/simp1.lua
@@ -17,6 +17,7 @@ parse_lean_cmds([[
 add_rewrite_rules("a_eq_1")
 add_rewrite_rules("f_id")
 add_rewrite_rules("eq_id")
+
 -- set_option({"lean", "pp", "implicit"}, true)
 e, pr = simplify(parse_lean('fun x, f (f x (0 + a)) (g (b + 0))'))
 print(e)