Monotype Proof Tree Editor
Write a proof tree for the following judgement:
Let in .
Each line of your tree should have the following components:
- a number followed by a period to indicate its depth in the tree. 0 is the root.
- a Gamma, in the form G, G (where is an integer) or as a set of variable type assignments.
- An expression.
- A type name. Type names are capitalized.
- A rule name in parenthesis.
If you use G or G1, etc. in your proof tree, you must follow the tree with their expanded out definitions.
The starter code shows a valid tree for a proof of .
Here are the monotype rules.
Proof Tree Editor