diff --git a/src/library/simplifier/ceqv.cpp b/src/library/simplifier/ceqv.cpp
index 6656f2747..57d06684c 100644
--- a/src/library/simplifier/ceqv.cpp
+++ b/src/library/simplifier/ceqv.cpp
@@ -37,6 +37,10 @@ class to_ceqvs_fn {
         return is_constant(fn) && ::lean::is_trans_relation(m_env, const_name(fn)) && is_type(e);
     }
 
+    bool is_relation(expr const & e) {
+        return is_transitive(e);
+    }
+
     list<expr_pair> lift(expr const & local, list<expr_pair> const & l) {
         lean_assert(is_local(local));
         return map(l, [&](expr_pair const & e_H) {
@@ -44,26 +48,32 @@ class to_ceqvs_fn {
             });
     }
 
-    list<expr_pair> apply(expr const & e, expr const & H) {
+    bool is_prop(expr const & e) {
+        constraint_seq cs;
+        return m_tc.is_prop(e, cs) && !cs;
+    }
+
+    // If restricted is true, we don't use (e <-> true) rewrite
+    list<expr_pair> apply(expr const & e, expr const & H, bool restrited) {
         expr c, Hdec, A, arg1, arg2;
-        if (is_transitive(e)) {
+        if (is_relation(e)) {
             return mk_singleton(e, H);
         } else if (is_standard(m_env) && is_not(m_env, e, arg1)) {
-            expr new_e = mk_iff(e, mk_false());
+            expr new_e = mk_iff(arg1, mk_false());
             expr new_H = mk_app(mk_constant(get_iff_false_intro_name()), arg1, H);
             return mk_singleton(new_e, new_H);
         } else if (is_standard(m_env) && is_and(e, arg1, arg2)) {
             // TODO(Leo): we can extend this trick to any type that has only one constructor
             expr H1 = mk_app(mk_constant(get_and_elim_left_name()), arg1, arg2, H);
             expr H2 = mk_app(mk_constant(get_and_elim_right_name()), arg1, arg2, H);
-            auto r1 = apply(arg1, H1);
-            auto r2 = apply(arg2, H2);
+            auto r1 = apply(arg1, H1, restrited);
+            auto r2 = apply(arg2, H2, restrited);
             return append(r1, r2);
         } else if (is_pi(e)) {
             expr local = mk_local(m_tc.mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e));
             expr new_e = instantiate(binding_body(e), local);
             expr new_H = mk_app(H, local);
-            auto r = apply(new_e, new_H);
+            auto r = apply(new_e, new_H, restrited);
             unsigned len = length(r);
             if (len == 0) {
                 return r;
@@ -72,7 +82,7 @@ class to_ceqvs_fn {
             } else {
                 return lift(local, r);
             }
-        } else if (is_standard(m_env) && is_ite(e, c, Hdec, A, arg1, arg2)) {
+        } else if (is_standard(m_env) && is_ite(e, c, Hdec, A, arg1, arg2) && is_prop(e)) {
             // TODO(Leo): support HoTT mode if users request
             expr not_c = mk_not(m_tc, c);
             expr Hc    = mk_local(m_tc.mk_fresh_name(), c);
@@ -81,28 +91,34 @@ class to_ceqvs_fn {
                                  c, arg1, arg2, Hdec, e, Hc});
             expr H2    = mk_app({mk_constant(get_implies_of_if_neg_name()),
                                  c, arg1, arg2, Hdec, e, Hnc});
-            auto r1    = lift(Hc, apply(arg1, H1));
-            auto r2    = lift(Hnc, apply(arg2, H2));
+            auto r1    = lift(Hc, apply(arg1, H1, restrited));
+            auto r2    = lift(Hnc, apply(arg2, H2, restrited));
             return append(r1, r2);
-        } else {
+        } else if (!restrited) {
             constraint_seq cs;
             expr new_e = m_tc.whnf(e, cs);
             if (new_e != e && !cs) {
-                return apply(new_e, H);
-            } else if (is_standard(m_env)) {
+                if (auto r = apply(new_e, H, true))
+                    return r;
+            }
+            if (is_standard(m_env) && is_prop(e)) {
                 expr new_e = mk_iff(e, mk_true());
                 expr new_H = mk_app(mk_constant(get_iff_true_intro_name()), arg1, H);
                 return mk_singleton(new_e, new_H);
             } else {
                 return list<expr_pair>();
             }
+        } else {
+            return list<expr_pair>();
         }
     }
 public:
     to_ceqvs_fn(type_checker & tc):m_env(tc.env()), m_tc(tc) {}
 
     list<expr_pair> operator()(expr const & e, expr const & H) {
-        return filter(apply(e, H), [&](expr_pair const & p) { return is_ceqv(m_tc, p.first); });
+        bool restrited = false;
+        list<expr_pair> lst = apply(e, H, restrited);
+        return filter(lst, [&](expr_pair const & p) { return is_ceqv(m_tc, p.first); });
     }
 };