(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 3 1 1

1. a : 
2. (a ~ 1)
3. b:b | a  (b ~ 1)  (b ~ a)
4. b : 
5. c : 
6. (b ~ 1)
7. (c ~ 1)
8. a = bc
  b | a


By: Witness c


Generated subgoals:

None

About:
intnatural_numbermultiplyequalimpliesorall
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