IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one one corr 2 functionality wrt eq1 1. A : Type
2. A' : Type
3. B : Type
4. B' : Type
5. A = A' 6. B = B' (A ~ B) = (A' ~ B')
By:
Subst: A = A' Type | B = B' Type
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(A ~ B) = (A' ~ B')
Type | B = B' 
