
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.
df6f1918
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.