Nuprl - Proof: firstn upto

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

n,m:

. firstn(n;upto(m)) ~ if n

upto(n) else upto(m) fi

By:	UnivCD THEN SplitOnConclITE

Generated subgoals:

1 1. n :
2. m :
3. nm
firstn(n;upto(m)) ~ upto(n)
5 steps

2 1. n :
2. m :
3. m<n
firstn(n;upto(m)) ~ upto(m)
1 step

About:

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

1	1. n : 2. m : 3. nm firstn(n;upto(m)) ~ upto(n)	5 steps
2	1. n : 2. m : 3. m<n firstn(n;upto(m)) ~ upto(m)	1 step