IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq atom eq true elim sqequal111 1. x : Atom
2. y : Atom
3. x=yAtom ~ true
4. x=yAtom = true
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