(10steps total) Remark Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub inj factorial2 1 1 1
  !(0 inj 0)
By: BackThru: Thm*  (A)  (!(A inj B))

Generated subgoal:

1   (0)
2 steps

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

(10steps total) Remark Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc