(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 1 2
1. a : 
2. a' : 
3. a'-a = 1
4. B : {a..a'}Type
5. a  {a:}
  B  {a:}Type
By: FunExtensionality

Generated subgoal:

1 6. x : {a:}
  x  {a..a'}
1 step

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

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