diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index a37bf8ae5..540eaf450 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -1389,7 +1389,7 @@ class elaborator::imp {
             } else if (is_abstraction(b)) {
                 imitate_abstraction(a, b, c);
                 return true;
-            } else if (is_app(b) && !has_metavar(arg(b, 0))) {
+            } else if (is_app(b) && (is_var(arg(b, 0)) || is_constant(arg(b, 0)) || is_value(arg(b, 0)))) {
                 imitate_application(a, b, c);
                 return true;
             } else if (is_proj(b)) {