Thm* Assignment 
Type
formula)+(formulaformula)+(formulaformula))
Thm* Formula Type
== Unit+Unit+Unit
Thm* Type
== inl(
)
Thm* 3
== inr(inr())
Thm* 3
Thm* Var Type
| Assignment |
Def Assignment == Var
Thm* Assignment |
| Formula |
Def Formula
== rec(formula.Var+formula+(formulaformula)+(formulaformula)+(formulaformula))
Thm* Formula |
| Three |
Def == Unit+Unit+Unit
Thm* |
| Three_0 |
Def 3 == inl()
Thm* 3 |
| Three_2 |
Def 3 == inr(inr())
Thm* 3 |
| Var |
Def Var == Atom
Thm* Var |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |