diff --git a/src/Bergamot/Latex.elm b/src/Bergamot/Latex.elm
index 683f1cb..d4909f5 100644
--- a/src/Bergamot/Latex.elm
+++ b/src/Bergamot/Latex.elm
@@ -68,4 +68,5 @@ metavariableToLatex (MkMetavariable s) =
         noQuestion = String.dropLeft 1 s
     in
         if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
-        if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion
+        if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else
+        if String.startsWith "rho" noQuestion then "\\" ++ noQuestion else noQuestion
diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm
index d2cb507..b05ac9f 100644
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@@ -158,6 +158,10 @@ builtinRules t =
             Call "int" [Var output] ->
                 let rec i = interleave (suggest "BuiltinInt" (IntLit i) output) (lazy <| \_ -> rec (i+1))
                 in rec 0
+            Call "add" [IntLit i1, IntLit i2, Var output] ->
+                suggest "BuiltinAdd" (IntLit (i1 + i2)) output
+            Call "subtract" [IntLit i1, IntLit i2, Var output] ->
+                suggest "BuiltinSubtract" (IntLit (i1 - i2)) output
             Call "float" [FloatLit f] ->
                 MkProofTree { name = "BuiltinFloat", conclusion = t, premises = [] }
                 |> pure