Def ActionSet(T) == car:TypeTcarcar

Thm* T:Type{i}. ActionSet(T) Type{i'}

Def z@x == z @ x

Thm* A:Type, R:(A*A*Prop). (EquivRel x,y:A*. x R y) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (z:A*, y:x,y:A*//(x R y). z@y x,y:A*//(x R y))

Def as @ bs == Case of as; nil bs ; a.as' a.(as' @ bs) (recursive)

Thm* T:Type, as,bs:T*. (as @ bs) T*

Def p = q == if p q else q fi

Thm* p,q:. p = q

Def Dec(P) == P P

Thm* A:Prop. Dec(A) Prop

Thm* T:Type, E:(TTProp). (EquivRel x,y:T. E(x,y)) Prop

Def Fin(s) == n:, f:(ns). Bij(n; s; f)

Thm* T:Type. Fin(T) Prop

Def (S:Ls) == if null(L) s else S.act(hd(L),(S:tl(L)s)) fi (recursive)

Thm* Alph:Type, S:ActionSet(Alph), L:Alph*, s:S.car. (S:Ls) S.car

Def b == if b false else true fi

Thm* b:. b

Def {i..j} == {k:| i k < j }

Thm* m,n:. {m..n} Type

Def == {i:| 0i }

Thm* Type

Def AB == B < A

Thm* i,j:. ij Prop

Def A == A False

Thm* A:Prop. (A) Prop

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

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

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

Thm* A,B:Type, f:(AB). Bij(A; B; f) Prop

Def tl(l) == Case of l; nil nil ; h.t t

Thm* A:Type, l:A*. tl(l) A*

Def hd(l) == Case of l; nil "?" ; h.t h

Thm* A:Type, l:A*. ||l||1 hd(l) A

Thm* T:Type, a:ActionSet(T). a.act Ta.cara.car

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

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

Thm* null(nil)

Def Surj(A; B; f) == b:B. a:A. f(a) = b

Thm* A,B:Type, f:(AB). Surj(A; B; f) Prop

Def Inj(A; B; f) == a1,a2:A. f(a1) = f(a2) B a1 = a2

Thm* A,B:Type, f:(AB). Inj(A; B; f) Prop

Thm* A:Type, B:(AType), p:a:AB(a). 2of(p) B(1of(p))