IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
harb wd
1
1
1
4
1
1. 'a : S
2. z : S
3. z = 'a
4. x : z
5. lem(z) = inl(x)
x 
'a
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
