IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length firstn21 1. A : Type
2. A List
3. u : A 4. v : A List
5. n:{0...||v||}. ||firstn(n;v)|| = n 6. n : {0...||u.v||}
7. 0<n ||firstn(n-1;v)||+1 = n
By:
RWW "5" 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
n:{0...||v||}. ||firstn(n;v)|| = n
||firstn(n-1;v)||+1 = n
