Def (n)! == if n=0 1 else n(n-1)! fi (recursive)

Thm* n:. (n)!

Def AB == B < A

Thm* i,j:. ij Prop

Def i=j == if i=j true ; false fi

Thm* i,j:. i=j

Def A == A False

Thm* A:Prop. (A) Prop