diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp
index 4ff379d2c9..dfdd300a90 100644
--- a/src/library/compiler/preprocess.cpp
+++ b/src/library/compiler/preprocess.cpp
@@ -91,7 +91,7 @@ class expand_aux_fn : public compiler_step_visitor {
     virtual expr visit_app(expr const & e) override {
         switch (get_recursor_app_kind(e)) {
         case recursor_kind::NotRecursor: {
-            if (is_not_vm_function(e)) {
+            if (is_not_vm_function(e) && !ctx().is_proof(e)) {
                 if (auto r = unfold_term(env(), e)) {
                     return visit(*r);
                 }