(3steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select tl
  A:Type, as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)]
By: (CDToVarThen `as' Analyze) THEN (Reduce 0) THEN RepD

Generated subgoals:

1 1. A : Type
2. A List
3. n : (-1)
  nil[n] = nil[(n+1)]  A
Auto
2 1. A : Type
2. A List
3. u : A
4. v : A List
5. n : (||v||+1-1)
  v[n] = (u.v)[(n+1)]
1 step

About:
listconsnilnatural_numberaddsubtractuniverseequalall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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