Add injectivity to peano

It is useful to have an axiom in mach.peano.Peano that:

axiom injectivity: forall x y: Peano.t. (x:int) = y -> x = y

The meta reason is that Peano.t is in fact a record with an invariant! (which should have injectivity #287 (closed)).