assert	Def b == if b True else False fi Thm* b:. b Prop
equiv_rel	Def EquivRel x,y:T. E(x;y) == Refl(T;x,y.E(x;y)) & Sym x,y:T. E(x;y) & Trans x,y:T. E(x;y) Thm* T:Type, E:(TTProp). (EquivRel x,y:T. E(x,y)) Prop
min_el	Def Min{ x | xEn } == MinArg(E(n) : {0..n}) Thm* E:(), n:. Min{ x | xEn }
nat	Def == {i:| 0i } Thm* Type
rev_implies	Def P Q == Q P Thm* A,B:Prop. (A B) Prop
trans	Def Trans x,y:T. E(x;y) == a,b,c:T. E(a;b) E(b;c) E(a;c) Thm* T:Type, E:(TTProp). Trans x,y:T. E(x,y) Prop
sym	Def Sym x,y:T. E(x;y) == a,b:T. E(a;b) E(b;a) Thm* T:Type, E:(TTProp). Sym x,y:T. E(x,y) Prop
refl	Def Refl(T;x,y.E(x;y)) == a:T. E(a;a) Thm* T:Type, E:(TTProp). Refl(T;x,y.E(x,y)) Prop
min_arg	Def MinArg(f : {0..n}) == n-MinAr(f;n;n) Thm* f:(), n:. MinArg(f : {0..n}) (n+1)
le	Def AB == B < A Thm* i,j:. ij Prop
min_ar	Def MinAr(f;i;n) == if (f(n-i))=(f(n)) i else MinAr(f;i-1;n) fi (recursive) Thm* f:(), n:, i:(n+1). MinAr(f;i;n) (i+1)
not	Def A == A False Thm* A:Prop. (A) Prop
eq_bool	Def p=q == (pq) (pq) Thm* p,q:. p=q
bnot	Def b == if b false else true fi Thm* b:. b
band	Def pq == if p q else false fi Thm* p,q:. (pq)
bor	Def p q == if p true else q fi Thm* p,q:. (p q)

About: