(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 2
1. a : 
2. b : 
  (i:b(a-1) inj {x:b| x = i }) ~ (b((a-1) inj (b-1)))
By: Rewrite by Thm*  k:, j:k. {i:k| i = j } ~ (k-1)

Generated subgoals:

None

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

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