IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc sequence rel wf1122 1. A : Type
2. a : A 3. e : AA 4. i : 5. i1:. i1<ii1 steps of e from aA 6. i 0
i-1 steps of e from aA
By:
BackThru: Hyp:5
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A
i1:
i1 steps of e from a 
A
0
i-1 steps of e from a 
