(3steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card sum family singleton vs intseg 1 1
1. a : 
2. a' : 
3. a'-a = 1
4. B : {a..a'}Type
  (i:{a..a'}B(i)) =ext ({a:}B(a))
By: BackThru: 
Thm*  a,a':.
Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a)))

Generated subgoals:

None

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

(3steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc