## range types should introduce an injectivity axiom

a range type declaration

`type t = range < a b >`

generates a function `t'int`

with an axiom

`forall x:t. a <= t'int x <= b`

but does NOT introduce any injectivity property such as

`forall x y:t. t'int x = t'int y -> x = y (*1*)`

Note that the form (1) is not easy to handle by solver. A potential interesting variant is introducing a reverse function

`function t'ofInt int : t`

with axiom

`forall x:t. t'ofInt (t'int x) = x (*2*)`

This variant has the advantage of avoiding a potential quadratic number of instanciations, as it is the case for (1)