(Formula List)
Thm* Sequent 
Type
formula)+(formulaformula)+(formulaformula))
Thm* Formula Type
T == 
x:S. x T
Thm* Var Type
| Sequent |
Def Sequent == (Formula List)(Formula List)
Thm* Sequent |
| Formula |
Def Formula
== rec(formula.Var+formula+(formulaformula)+(formulaformula)+(formulaformula))
Thm* Formula |
| subtype |
Def S T == x:S. x T
|
| Var |
Def Var == Atom
Thm* Var |
About:
 |  |  |  |  |
 |  |  |  |