-
Robbert Krebbers authored
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.
030b0fb6
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.