The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Adam Chlipala wrote:
> Your example is strange.  Up to proof irrelevance, the type [BSig] has 
> exactly one inhabitant (which is [Build_B "kilometers"]), so the 
> coercion must be the constant function returning that value.

I actually meant that the inhabitant is the value I gave injected into 
[BSig] with a [refl_equal] proof of the equality fact.