diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 1a3a53ef8c..a0b2d260b3 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -101,7 +101,7 @@ public:
     virtual expr get_type() const { return m_type; }
     virtual name get_name() const { return g_if_name; }
     virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 5 && is_bool_value(args[2])) {
+        if (num_args == 5 && is_bool_value(args[2]) && is_value(args[3]) && is_value(args[4])) {
             if (to_bool(args[2]))
                 return some_expr(args[3]); // if A true a b  --> a
             else
diff --git a/tests/lean/tst10.lean.expected.out b/tests/lean/tst10.lean.expected.out
index 5ba3288e85..f57a72c9ae 100644
--- a/tests/lean/tst10.lean.expected.out
+++ b/tests/lean/tst10.lean.expected.out
@@ -16,7 +16,7 @@ a ∨ a ∨ b
 a ⇒ b ⇒ a
 a ⇒ b : Bool
 if a a ⊤
-a
+if ⊤ a ⊤
   Assumed: H1
   Assumed: H2
 @MP : Π (a b : Bool), (a ⇒ b) → a → b