(5steps total) PrintForm Definitions list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select cons tl

  T:Type, a:Tas:T List, i:. 0<i  i||as||  (a.as)[i] = as[(i-1)]

By: UnivCD


Generated subgoal:

1 1. T : Type
2. a : T
3. as : T List
4. i : 
5. 0<i
6. i||as||
  (a.as)[i] = as[(i-1)]

4 steps

About:
listconsintnatural_numbersubtractless_thanuniverseequalimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(5steps total) PrintForm Definitions list 1 Sections StandardLIB Doc