IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq atom eq false elim sqequal111 1. x : Atom
2. y : Atom
3. x=yAtom ~ false 4. x=yAtom = false x = y
By:
RW bool_to_propC -1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html