interface Injective : (a -> b) -> Type
An injective function maps distinct elements to distinct elements.
injective : f x = f y -> x = y
injective : Injective f => f x = f y -> x = y
inj : (0 f : (a -> b)) -> {auto 0 _ : Injective f} -> (0 _ : f x = f y) -> x = y