(12steps total) PrintForm Definitions core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable atom equal 1 1 4 1
1. a : Atom
2. b : Atom
3. a = b
  (x.x)  (a = b)
By: Unfold `not` 0 THEN Analyze

Generated subgoals:

1 4. x : a = b
  x  False
Trivial
2   (a = b)  Type
Auto

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

(12steps total) PrintForm Definitions core StandardLIB Doc