assert	Def b == if b True else False fi Thm* b:. b Prop
lang_eq	Def L = M == l:Alph*. L(l) M(l) Thm* Alph:Type{i}, L,M:LangOver(Alph). L = M Prop{i'}
iff	Def P Q == (P Q) & (P Q) Thm* A,B:Prop. (A B) Prop
languages	Def LangOver(Alph) == Alph*Prop Thm* Alph:Type{i}. LangOver(Alph) Type{i'}
nat	Def == {i:| 0i } Thm* Type
null	Def null(as) == Case of as; nil true ; a.as' false Thm* T:Type, as:T*. null(as) Thm* null(nil)
rev_implies	Def P Q == Q P Thm* A,B:Prop. (A B) Prop
le	Def AB == B < A Thm* i,j:. ij Prop
not	Def A == A False Thm* A:Prop. (A) Prop

About: