| Some definitions of interest. |
|
le | Def AB == B<A |
| | Thm* i,j:. (ij) Prop |
|
length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | Thm* A:Type, l:A List. ||l|| |
| | Thm* ||nil|| |
|
select | Def l[i] == hd(nth_tl(i;l)) |
| | Thm* A:Type, l:A List, n:. 0n n<||l|| l[n] A |