IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
inhabited uniquely vs exists unique1111 1. A : Type
2. x : A 3. y:A. x = y 4. y : A 5. True
y = x
By:
BackThru: Hyp:3
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html