(7steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: firstn upto 2
1. n : 
2. m : 
3. m<n
  firstn(n;upto(m)) ~ upto(m)
By: RWO Thm* L:Top List, n:. ||L||n  (firstn(n;L) ~ L) 0
THEN
RWO Thm* n:. ||upto(n)|| ~ n 0

Generated subgoals:

None

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

(7steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc