IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
member iff sublist21 1. T : Type
2. x : T 3. L : T List
4. f : 1||L||
5. increasing(f;1)
6. j:1. [x][j] = L[(f(j))]
x = L[(f(0))]
By:
InstHyp [0] -1 THEN Reduce -1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
1
j:
x = L[(f(0))]
