(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 1 1
1. k : 
2. k1:. k1<k  (x,y:. x+y = k1  (a:. nat_to_nat_pair(a) = <x,y>))
3. x : 
4. x1:. x1<x  (y:. x1+y = k  (a:. nat_to_nat_pair(a) = <x1,y>))
5. y : 
6. x+y = k
  a:. nat_to_nat_pair(a) = <x,y>
By: Decide: x = 0 THENL [Decide: y = 0;Id]

Generated subgoals:

1 7. x = 0
8. y = 0
  a:. nat_to_nat_pair(a) = <x,y>
2 steps
2 7. x = 0
8. y = 0
  a:. nat_to_nat_pair(a) = <x,y>
5 steps
3 7. x = 0
  a:. nat_to_nat_pair(a) = <x,y>
6 steps

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

(19steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc