IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nat to nat pair surj111211 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 7. x = 0
8. y = 0
9. n : 10. nat_to_nat_pair(n) = <y-1,0>
nat_to_nat_pair(n+1) = <x,y>
By:
Compute nat_to_nat_pair(n+1) THEN SplitITE Concl THEN Subst: n+1-1 = n