(18steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: next nat pair vs prev nat pair 2 1 2
1. y1 : 
2. y2 : 
3. <y1,y2> = <0,0>
  next_nat_pair(prev_nat_pair(<y1,y2>)) = <0,0>  
By: Hyp:3  Asserted THEN SimilarTo: Hyp:-1

Generated subgoals:

1 4. next_nat_pair(prev_nat_pair(<y1,y2>)) = <0,0>  
  <y1,y2> = <0,0>  
6 steps
2 4. <y1,y2> = <0,0>  
  (next_nat_pair(prev_nat_pair(<y1,y2>)) = <0,0>  )  Prop
2 steps

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

(18steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc