diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm
index 90df3d8..0f0cf5d 100644
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@@ -33,6 +33,9 @@ andThen f p env ps =
     p env ps
     |> Search.andThen (\(a, psp) -> (f a) env psp)
 
+join : Prover (Prover a) -> Prover a
+join p = andThen (\x -> x) p
+
 apply : Prover a -> Prover (a -> b) -> Prover b
 apply pa pf = pf |> andThen (\f -> map f pa)
 
@@ -91,10 +94,12 @@ provePremises l =
             |> apply (provePremises ts)
         [] -> pure []
 
-prove : Term UnificationVar -> Prover ProofTree
-prove t =
-    getEnv
-    |> andThen (List.foldl (\r -> interleave (rule t r)) fail << .rules)
+prove : Term Metavariable -> Prover ProofTree
+prove mt =
+    pure (\t env -> List.foldl (\r -> interleave (rule t r)) fail env.rules)
+    |> apply (liftInstantiation instantiate mt)
+    |> apply getEnv
+    |> join
 
 single : RuleEnv -> Prover a -> Maybe a
 single env p =