diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 1d2ad30e36..d97a80a610 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -774,13 +774,13 @@ bool type_checker::is_def_eq_app(expr const & t, expr const & s) {
 
 /** \brief Return true if \c t and \c s are definitionally equal due to proof irrelevant.
     Return false otherwise. */
-bool type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) {
+lbool type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) {
     // Proof irrelevance support for Prop (aka Type.{0})
     expr t_type = infer_type(t);
     if (!is_prop(t_type))
-        return false;
+        return l_undef;
     expr s_type = infer_type(s);
-    return is_def_eq(t_type, s_type);
+    return to_lbool(is_def_eq(t_type, s_type));
 }
 
 bool type_checker::failed_before(expr const & t, expr const & s) const {
@@ -938,8 +938,8 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
         if (r != l_undef) return r == l_true;
     }
 
-    if (is_def_eq_proof_irrel(t_n, s_n))
-        return true;
+    r = is_def_eq_proof_irrel(t_n, s_n);
+    if (r != l_undef) return r == l_true;
 
     r = lazy_delta_reduction(t_n, s_n);
     if (r != l_undef) return r == l_true;
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 60c25b86a4..a5fcd4612e 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -81,7 +81,7 @@ private:
     lbool try_string_lit_expansion_core(expr const & t, expr const & s);
     lbool try_string_lit_expansion(expr const & t, expr const & s);
     bool is_def_eq_app(expr const & t, expr const & s);
-    bool is_def_eq_proof_irrel(expr const & t, expr const & s);
+    lbool is_def_eq_proof_irrel(expr const & t, expr const & s);
     bool failed_before(expr const & t, expr const & s) const;
     void cache_failure(expr const & t, expr const & s);
     reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n);