Todd Wilson answered my query by politely pointing out the obvious-- that the function g:N-->N^N with g(m) = (lambda n)(sn+m) is defined by the same induction on NxN as the function g':N-->NxN with g'(m) = (lambda m)(m+sn). Namely, g(0) = successor, and gs = sg. And so the function h:N-->N^N with h(m) = (lambda n)(m+n) is defined by the same induction as h'(m)=(lambda n)(n+m), namely h(0)= 1_N and hs=sh. I'm afraid I manufactured a difficulty by focussing on Cartesian Closed categories as "less than toposes" rather than thinking of them in their own terms--so the "Peano axiom" kind of proof I was looking for is unavailable, but no problem. Colin