PeanoEqual(a,    b) =    # a and b are both nonzero
     PeanoEqual(a-1, b-1)  # so recurse

Subtracting Peano literals would involve some constraints in the type, so shouldn't that be (a+1,b+1) for typing purposes?