Def Sequent == (Formula List)(Formula List)

Thm* Sequent Type

Def Formula == rec(formula.Var+formula+(formulaformula)+(formulaformula)+(formulaformula))

Thm* Formula Type

Thm* Var Type