(31steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card nsub inj vs lopped 1 1 1 1
1. a : 
2. b : 
3. f : a inj b
  f(a-1)  b
By: Analyze-1

Generated subgoals:

None

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

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