| Some definitions of interest. |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
nat_to_nat_pair | Def nat_to_nat_pair(i) == next_nat_pair{ i}(<0,0>) |
| | Thm* nat_to_nat_pair       |
|
nequal | Def a b T == a = b T |
| | Thm* A:Type, x,y:A. (x y) Prop |
|
next_nat_pair | Def next_nat_pair(xy) == xy/x,y. if y= 0 <0,x+1> else <x+1,y-1> fi |
| | Thm* next_nat_pair         |