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

Thm* Sequent Type

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

Thm* Formula Type

Def Discrete{T} == x,y:T. Dec(x = y)

Thm* T:Type{i}. Discrete{T} Type{i'}

Thm* Var Type

Def Dec(P) == P P

Thm* A:Prop. Dec(A) Prop

Def A == A False

Thm* A:Prop. (A) Prop