IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
least wf21 1. p : {p:()| i:. p(i) }
2. (least i:. p(i)) {i:| p(i) & (j:. j<ip(j)) }
(least i:. p(i))
By:
BackThru: {i:| p(i) & (j:. j<ip(j)) }
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
)| 
i:
{i:
j:
p(j)) }
(least i:
