IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc equal via so12 1. A : Type
2. a : A 3. b : A 4. P:(AProp). P(a) P(b)
a = b
By:
Inst: Hyp:-1 Using:[P(x):= a = xA]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
P:(A
Prop). P(a) 
P(b)
a = b
A]
