(13steps 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: before-upto
  n:, x,y:n. x before y  upto(n)  x<y
By: Unfold `l_before` 0 THEN Unfold `sublist` 0 THEN Reduce 0 THEN Reduce 0
THEN
ExRepD

Generated subgoals:

1 1. n : 
2. x : n
3. y : n
4. f : 2||upto(n)||
5. increasing(f;2)
6. j:2. [x; y][j] = upto(n)[(f(j))]
  x<y
4 steps
2 1. n : 
2. x : n
3. y : n
4. x<y
  f:(2||upto(n)||). increasing(f;2) & (j:2. [x; y][j] = upto(n)[(f(j))])
8 steps

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

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