| Some definitions of interest. | |
| int_seg |  } == {k:  | i  k < j } | 
|  m,n:  . {m..n  }  Type | |
| length |  0 ; a.as'  ||as'||+1  (recursive) | 
|  A:Type, l:A List. ||l||    | |
|    | |
| listify |  } == if n   m  nil else f(m).f{(m+1)..n  } fi  (recursive) | 
|  T:Type, m,n:  , f:({m..n  }   T). f{m..n  }  T List | 
About:
|  |  |  |  | 
|  |  |  |  |  |  | 
|  |  |  |  |  | 
|  |