IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The last subgoal of the proof of Thm* A 
Top,
1. A : Type
2. x : A
x 
Top
does
not simply mean that every notation of (supposed) type A is also a notation of type Top.
It means further that if a = b A then a = b Top.
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
