(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
  a,b:Atom. Dec(a = b)
By: (Unfold `decidable` 0) THEN RepD

Generated subgoal:

1 1. a : Atom
2. b : Atom
  a = b  a = b
11 steps

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

(12steps total) PrintForm Definitions core StandardLIB Doc