(7steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select nth tl
  T:Type, as:T List, n:{0...||as||}, i:(||as||-n).
  nth_tl(n;as)[i] = as[(i+n)]
By: (CDToVarThen `as' ListInd) THEN (Reduce 0)

Generated subgoals:

1 1. T : Type
2. T List
  n:{0...0}, i:(0-n). nth_tl(n;nil)[i] = nil[(i+n)]  T
Auto
2 1. T : Type
2. T List
3. u : T
4. v : T List
5. n:{0...||v||}, i:(||v||-n). nth_tl(n;v)[i] = v[(i+n)]
  n:{0...||v||+1}, i:(||v||+1-n). nth_tl(n;u.v)[i] = (u.v)[(i+n)]
5 steps

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

(7steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc