diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 091fef858..debff5475 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -823,7 +823,7 @@ bool is_elim_meta_app_core(Ctx & ctx, expr const & e) {
     if (elim_args.size() < major_idx + 1)
         return false;
     expr intro_app = ctx.whnf(elim_args[major_idx]);
-    return has_expr_metavar(intro_app);
+    return has_expr_metavar_strict(intro_app);
 }
 
 bool is_elim_meta_app(type_checker & tc, expr const & e) {
diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp
index 4d7bd32a7..f2796fec5 100644
--- a/src/library/inductive_unifier_plugin.cpp
+++ b/src/library/inductive_unifier_plugin.cpp
@@ -52,7 +52,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
         unsigned elim_num_lvls = length(elim_lvls);
         unsigned major_idx     = *inductive::get_elim_major_idx(env, const_name(elim));
         expr meta              = args[major_idx]; // save this argument, we will update it
-        lean_assert(has_expr_metavar(meta));
+        lean_assert(has_expr_metavar_strict(meta));
         buffer<expr> margs;
         expr const & m     = get_app_args(meta, margs);
         expr mtype = tc.infer(m, tc_cnstr_buffer);