[Agda] Constructors are injective -- standard proof?

[Helmut Grohne]

On Thu, Jun 05, 2014 at 10:20:28AM -0400, Jacques Carette wrote:
> Specific question: Is the proof that 'suc' is injective in the
> standard library?  I searched for it, and could not find it.  [Of
> course it is trivial, but it seems silly to rewrite this over and
> over again, which is what a 'standard' library is for].

cong pred

Helmut