Prove UIP for decidable types without relying on the stdlib.

This way we get rid of the (unused) axiom eq_rect_eq reported by coqchk.
1 job for master in 8 minutes and 53 seconds (queued for 1 second)
Status Job ID Name Coverage
  Test
passed #665
coq
buildjob

00:08:53