(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
  (0 inj 0) ~ 1
By: BackThru: Thm*  (A ~ 1)  (!A)

Generated subgoal:

1   !(0 inj 0)
3 steps

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