Def L = M == l:Alph*. L(l) M(l)

Thm* Alph:Type{i}, L,M:LangOver(Alph). L = M Prop{i'}

Def (l) == null(l)

Thm* Alph:Type. LangOver(Alph)

Def LangOver(Alph) == Alph*Prop

Thm* Alph:Type{i}. LangOver(Alph) Type{i'}

Def P Q == (P Q) & (P Q)

Thm* A,B:Prop. (A B) Prop

Def null(as) == Case of as; nil true ; a.as' false

Thm* T:Type, as:T*. null(as)

Thm* null(nil)

Def b == if b True else False fi

Thm* b:. b Prop

Def P Q == Q P

Thm* A,B:Prop. (A B) Prop