diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 22b4b3395..b664a9e26 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -220,6 +220,9 @@ private:
 
             if (m_bv.is_numeral(arg, r) && r != mdl)
                 return false;
+
+            if (i > 0 && (!is_app(arg) || to_app(arg)->get_num_args() > 0))
+                return false;
         }
 
         if (mc) {