diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 69bcb5530..03b1b8c0f 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -594,7 +594,7 @@ struct unifier_fn {
         }
 
         // We delay constraints where lhs or rhs are of the form (elim ... (?m ...))
-        if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs)) {
+        if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs) || is_meta_intro_app(lhs) || is_meta_intro_app(rhs)) {
             add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs);
         } else if (is_meta(lhs) && is_meta(rhs)) {
             // flex-flex constraints are delayed the most.
@@ -834,6 +834,16 @@ struct unifier_fn {
         return is_eq_cnstr(c) && (is_elim_meta_app(cnstr_lhs_expr(c)) || is_elim_meta_app(cnstr_rhs_expr(c)));
     }
 
+    /** \brief Return true iff \c e is of the form (?m ... (intro ...)) */
+    bool is_meta_intro_app(expr const & e) {
+        if (!is_app(e) || !is_meta(e))
+            return false;
+        expr arg = get_app_fn(app_arg(e));
+        if (!is_constant(arg))
+            return false;
+        return (bool) inductive::is_intro_rule(m_env, const_name(arg)); // NOLINT
+    }
+
     /**
        \brief Given (elim args) =?= t, where elim is the eliminator/recursor for the inductive declaration \c decl,
        and the last argument of args is of the form (?m ...), we create a case split where we try to assign (?m ...)