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