diff --git a/src/Bergamot/Syntax.elm b/src/Bergamot/Syntax.elm
index f09f8b4..15cc4fe 100644
--- a/src/Bergamot/Syntax.elm
+++ b/src/Bergamot/Syntax.elm
@@ -7,6 +7,7 @@ import Tuple
 import Debug
 
 type alias Name = String
+type alias Metavariable = String
 type alias UnificationVar = String
 
 type Term a
@@ -15,6 +16,37 @@ type Term a
     | Call Name (List (Term a))
     | Var a
 
+type alias InstantiationState =
+    { counter : Int
+    , vars : Dict Metavariable UnificationVar
+    }
+
+metavariable : Metavariable -> InstantiationState -> (UnificationVar, InstantiationState)
+metavariable mv is =
+    case Dict.get mv is.vars of
+        Just v -> (v, is)
+        Nothing ->
+            let
+                v = "var" ++ (String.fromInt is.counter)
+                isp = { counter = is.counter + 1, vars = Dict.insert mv v is.vars }
+            in (v, isp)
+
+instantiateList : List (Term Metavariable) -> InstantiationState -> (List (Term UnificationVar), InstantiationState)
+instantiateList ml is =
+    case ml of
+        mt :: mts ->
+            instantiate mt is
+            |> \(t, isp) -> Tuple.mapFirst (\ts -> t :: ts) (instantiateList mts isp)
+        [] -> ([], is)
+
+instantiate : Term Metavariable -> InstantiationState -> (Term UnificationVar, InstantiationState)
+instantiate mt is =
+    case mt of
+        IntLit i -> (IntLit i, is)
+        StringLit s -> (StringLit s, is)
+        Call n mts -> Tuple.mapFirst (Call n) (instantiateList mts is)
+        Var mv -> Tuple.mapFirst Var (metavariable mv is)
+
 type alias UnificationInfo =
     { equivalence : Set UnificationVar
     , term : Maybe (Term UnificationVar)