(19steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat to nat pair surj 1
  b:(). a:. nat_to_nat_pair(a) = b
By: k,x,y:. x+y = k  (a:. nat_to_nat_pair(a) = <x,y>)  Asserted

Generated subgoals:

1   k,x,y:. x+y = k  (a:. nat_to_nat_pair(a) = <x,y>)
15 steps
2 1. k,x,y:. x+y = k  (a:. nat_to_nat_pair(a) = <x,y>)
  b:(). a:. nat_to_nat_pair(a) = b
2 steps

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

(19steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc