| Some definitions of interest. |
|
listp | Def A List == {l:(A List)| (0< ||l||) } |
| | Thm* A:Type. A List Type |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
ge | Def i j == j i |
| | Thm* i,j: . (i j) Prop |
|
length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | Thm* A:Type, l:A List. ||l||  |
| | Thm* ||nil||  |
|
lt_int | Def i< j == if i<j true ; false fi |
| | Thm* i,j: . (i< j)  |