diff --git a/src/Main.elm b/src/Main.elm
index 58fd050..0468319 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -221,7 +221,8 @@ viewProofTree : ResultMode -> Term Metavariable -> (RuleEnv, RuleEnv) -> Result
 viewProofTree resultMode query (prog, renderProg) =
     case single prog (prove query |> Bergamot.Rules.andThen reifyProofTree) of
         Just proofTree -> renderProofTree resultMode proofTree renderProg
-        Nothing -> Ok <| Html.div [ class "bergamot-no-proofs" ] []
+        Nothing -> Ok <| Html.div [ class "bergamot-no-proofs" ]
+            [ Html.text "No applicable rules to prove input" ]
 
 view : Model -> Html Msg
 view m =