diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm
index 0f0cf5d..a384f4c 100644
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@@ -90,16 +90,19 @@ provePremises l =
     case l of
         t :: ts ->
             pure (::)
-            |> apply (prove t)
+            |> apply (proveTerm t)
             |> apply (provePremises ts)
         [] -> pure []
 
+proveTerm : Term UnificationVar -> Prover ProofTree
+proveTerm t =
+    getEnv
+    |> andThen (\env -> List.foldl (\r -> interleave (rule t r)) fail env.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
+    liftInstantiation instantiate mt
+    |> andThen proveTerm
 
 single : RuleEnv -> Prover a -> Maybe a
 single env p =
diff --git a/src/Main.elm b/src/Main.elm
index 93bea8d..0921c0e 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -3,6 +3,7 @@ module Main exposing (main)
 import Browser
 import Html exposing (Html)
 import Html.Events exposing (onInput)
+import Html.Attributes exposing (type_)
 import Bergamot.Syntax exposing (..)
 import Bergamot.Search exposing (..)
 import Bergamot.Rules exposing (..)
@@ -11,24 +12,37 @@ import Maybe
 import Tuple
 import Debug
 
-type alias Model = { program : String }
+type alias Model =
+    { program : String
+    , query : String
+    }
 type alias Flags = ()
 type Msg
     = SetProgram String
+    | SetQuery String
 
 init : Flags -> (Model, Cmd Msg)
-init () = ({ program = "" }, Cmd.none)
+init () = ({ program = "", query = "" }, Cmd.none)
+
+proveQuery : String -> String -> Maybe ProofTree
+proveQuery progs querys =
+    case (run program progs, run term querys) of
+        (Just prog, Just query) -> single prog (prove query)
+        _ -> Nothing
 
 view : Model -> Html Msg
 view m = Html.div []
     [ Html.textarea [ onInput SetProgram ] []
-    , Html.p [] [ Html.text (Debug.toString (run program m.program)) ]
+    , Html.br [] []
+    , Html.input [ type_ "text", onInput SetQuery ] []
+    , Html.p [] [ Html.text (Debug.toString (proveQuery m.program m.query)) ]
     ]
 
 update : Msg -> Model -> (Model, Cmd Msg)
 update msg m =
     case msg of
         SetProgram prog -> ({ m | program = prog }, Cmd.none)
+        SetQuery query -> ({ m | query = query }, Cmd.none)
 
 subscriptions : Model -> Sub Msg
 subscriptions _ = Sub.none