Now really get rid of the eq_rect_eq axiom.

The previous commit is not really necesarry anymore, but my proof
for UIP of types with decidable equality is a bit more general, so
I won't revert it.