diff --git a/src/library/elaborator.cpp b/src/library/elaborator.cpp
index 3be884437..a2a22946b 100644
--- a/src/library/elaborator.cpp
+++ b/src/library/elaborator.cpp
@@ -123,6 +123,8 @@ class elaborator::imp {
             return level();
         } else if (is_type(e)) {
             return ty_level(e);
+        } else if (e == Bool) {
+            return level();
         } else {
             expr r = head_reduce_mmv(e, m_env, m_available_defs);
             if (!is_eqp(r, e)) {