IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc some via so1111 1. A : Type
2. B : AProp
3. x : A 4. B(x)
5. C : Prop
6. x:A. B(x) C C
By:
FwdThru: Hyp:-1 on [ B(x) ]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html