The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Michael Shulman wrote:
> Apparently the use of the UIP axiom can sometimes be avoided by a
> dependent elimination, as long as enough definitions are transparent.
> Are there reasons to prefer UIP in such situations?
>
> [...]
>
> A secondary question is, given that having transparent theorems is
> useful in situations such as this, what is the advantage of making them
> opaque by default?
>    

I like having theorems be opaque, since their insides almost never 
matter, and opacity forces the rest of a development to behave according 
to that abstraction.  It seems fine to me to use transparent theorems 
for special cases like this that need computation to work.  Also, real 
developments can almost always avoid these issues (i.e., explicit 
proofs/casts in programs) with clever structuring. :)