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

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

Def MinArg(f : {0..n}) == n-MinAr(f;n;n)

Thm* f:(), n:. MinArg(f : {0..n}) (n+1)

Def == {i:| 0i }

Thm* Type

Def P Q == Q P

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

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)

Def AB == B < A

Thm* i,j:. ij Prop

Def p=q == (pq) (pq)

Thm* p,q:. p=q

Def A == A False

Thm* A:Prop. (A) Prop

Def b == if b false else true fi

Thm* b:. b

Def pq == if p q else false fi

Thm* p,q:. (pq)

Def p q == if p true else q fi

Thm* p,q:. (p q)