(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. a : 
2. b : 
  (f.<f(a-1),f>)  (a inj b)(i:b(a-1) inj {x:b| x = i })
By: 2 Times Analyze

Generated subgoals:

1 3. f : a inj b
  f(a-1)  b
1 step
2 3. f : a inj b
  f  (a-1) inj {x:b| x = f(a-1) }
1 step

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

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