diff --git a/src/Bergamot/Latex.elm b/src/Bergamot/Latex.elm
index d0baf78..fb6a459 100644
--- a/src/Bergamot/Latex.elm
+++ b/src/Bergamot/Latex.elm
@@ -6,12 +6,20 @@ import Bergamot.Rules exposing (..)
 termToLatex : (a -> String) -> Term a -> String
 termToLatex f t =
     case t of
-        Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
         Call "intlit" [t1]   -> termToLatex f t1
         Call "strlit" [t1]   -> termToLatex f t1
-        Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
+        Call "var" [t1]   -> termToLatex f t1
         Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2
         Call "pair" [t1, t2] -> "(" ++ termToLatex f t1 ++ ", " ++ termToLatex f t2 ++ ")"
+        Call "abs" [t1, t2, t3] -> "\\lambda " ++ termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ ".\\ " ++ termToLatex f t3
+        Call "app" [t1, t2] -> termToLatex f t1 ++ "\\ " ++ termToLatex f t2
+        Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
+        Call "type" [t1, t2, t3] -> termToLatex f t1 ++ "\\vdash\\ " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
+        Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
+        Call "tarr" [t1, t2] -> termToLatex f t1 ++ "\\to" ++ termToLatex f t2
+        Call "extend" [t1, t2, t3] -> termToLatex f t1 ++ ",\\ " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
+        Call "inenv" [t1, t2, t3] -> termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ " \\in " ++ termToLatex f t3 
+        Call "empty" [] -> "\\varnothing"
         Call s [] -> "\\text{" ++ s ++ "}"
         Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
         Var x -> f x
@@ -23,7 +31,8 @@ metavariableToLatex (MkMetavariable s) =
     let
         noQuestion = String.dropLeft 1 s
     in
-        if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else noQuestion
+        if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
+        if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion
 
 ruleToLatex : Rule -> String
 ruleToLatex r = "\\cfrac{" ++ String.join "\\quad " (List.map (termToLatex metavariableToLatex) r.premises) ++ "}{" ++ termToLatex metavariableToLatex r.conclusion ++ "}\\ \\texttt{" ++ r.name ++ "}"
diff --git a/src/Bergamot/Parser.elm b/src/Bergamot/Parser.elm
index 81f706a..81d8f3f 100644
--- a/src/Bergamot/Parser.elm
+++ b/src/Bergamot/Parser.elm
@@ -27,8 +27,7 @@ variable =
 
 term : Parser (Term Metavariable)
 term = Parser.lazy (\() -> Parser.oneOf
-    [ Parser.succeed IntLit |= intLit
-    , Parser.backtrackable <|
+    [ Parser.backtrackable <|
       Parser.succeed Call
         |= name
         |= Parser.sequence
@@ -39,9 +38,12 @@ term = Parser.lazy (\() -> Parser.oneOf
             , item = term
             , trailing = Forbidden
             }
-    , Parser.succeed (\n -> Call n [])
+    , Parser.backtrackable <|
+      Parser.succeed (\n -> Call n [])
         |= name
-    , Parser.succeed Var |= variable
+    , Parser.backtrackable <|
+      Parser.succeed Var |= variable
+    , Parser.succeed IntLit |= intLit
     ])
 
 rule : Parser Rule