(9steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card prod family intseg singleton elim

  a,a':a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a))

By: Auto


Generated subgoal:

1 1. a : 
2. a' : 
3. a'-a = 1
4. B : {a..a'}Type
  (i:{a..a'}B(i)) ~ B(a)

8 steps

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

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