diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm
index ef9d541..a9d5a90 100644
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@@ -152,7 +152,7 @@ proveTerm t =
 
 prove : Term Metavariable -> Prover ProofTree
 prove mt =
-    liftInstantiation instantiate mt
+    withVars (liftInstantiation instantiate mt)
     |> andThen proveTerm
 
 single : RuleEnv -> Prover a -> Maybe a