1. Input a term in the text box.
    • a term consists of either a variable, a lambda abstraction, or an application.
    • a lower-case letter represents a variable.
    • a lambda abstraction is written as fun x -> term
    • an application is written as juxtaposition.
    • example: (fun x -> x) (fun y -> y)
  2. Press "go" button.
  3. Click judgement and press buttons to construct a proof tree.