Nuprl - Proof: firstn upto 1 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: firstn upto 1 2 2

1. n :

2. m :

3. n

firstn(n;upto(n)) ~ upto(n)

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:

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