(5steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prev nat pair wf 1 1

1. x : 
2. y : 
3. <x,y> = <0,0>
4. x = 0
  y-1  


By: y = 0    Asserted


Generated subgoal:

1   y = 0  
2 steps

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

(5steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc