| | Some definitions of interest. |
|
| IdLnk | Def IdLnk == Id Id |
| | | Thm* IdLnk  Type |
|
| rset | Def |R| == {i:Id|  (R(i)) } |
| | | Thm*  R:(Id   ). |R| Type |
|
| Id | Def Id == Atom |
| | | Thm* Id Type |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| fun_exp | Def f^n == primrec(n; x.x;i,g. f o g) |
| | | Thm* T:Type, n:, f:(TT). f^n TT |
|
| l_member | Def (x l) ==  i:. i<||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
| ldst | Def destination(l) == 1of(2of(l)) |
| | | Thm* l:IdLnk. destination(l) Id |
|
| length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | | Thm* A:Type, l:A List. ||l||  |
| | | Thm* ||nil|| |
|
| lsrc | Def source(l) == 1of(l) |
| | | Thm* l:IdLnk. source(l) Id |
|
| nat_plus | Def  == {i:| 0<i } |
| | | Thm* Type |
