(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 1

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


By: Analyze


Generated subgoals:

None

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

(5steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc