(2steps total) PrintForm Definitions Lemmas bool 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: neg assert of eq atom
  x,y:Atom. x=yAtom  x  y
By: UnivCD THEN (RWH (LemmaC Thm* x,y:Atom. x=yAtom  x = y) 0)

Generated subgoal:

1 1. x : Atom
2. y : Atom
  x = y  x  y
1 step

About:
assertatomequalall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(2steps total) PrintForm Definitions Lemmas bool 1 Sections StandardLIB Doc