Usage:

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.