IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq atom eq false elim sqequal12 1. x : Atom
2. y : Atom
(x=yAtom ~ false) Type
By:
Analyze
Generated subgoals:
1
x=yAtom ~ x=yAtom
Trivial
2
false ~ false
Trivial
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html