[Agda] injectivity of Data.Char.toNat?

[Nils Anders Danielsson]

On 2011-11-21 13:43, Ramana Kumar wrote:
> Is the following provable? How?
>
> foo₁ : (_≡_ on Data.Char.toNat) ⇒ _≡_
> foo₁ = ?

The function toNat is a primitive, for which no properties are provided,
so I don't see how you could prove this without "cheating".

-- 
/NAD