(22steps total) Remark PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: atomic char
  a:. atomic(a)  (a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))
By: Unfolds [`guard`;`atomic`] 0 THEN GenExRepD

Generated subgoals:

1 1. a : 
2. a = 0
3. (a ~ 1)
4. reducible(a)
5. b : 
6. b | a
  (b ~ 1)  (b ~ a)
7 steps
2 1. a : 
2. (a ~ 1)
3. b:. b | a  (b ~ 1)  (b ~ a)
  a = 0
4 steps
3 1. a : 
2. (a ~ 1)
3. b:. b | a  (b ~ 1)  (b ~ a)
  reducible(a)
10 steps

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

(22steps total) Remark PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc