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

  a,a':.
  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}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)) =ext ({a:}B(a))

6 steps

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

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