The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

If some type has decidable equality, then all proofs of the same 
equality in that type are provably equal.  See this module from the 
standard library:
    https://coq.inria.fr/stdlib/Coq.Logic.Eqdep_dec.html

It is also popular to assert as an axiom that all proofs of some 
equality are equal, though in general that property is independent of 
Coq's logical theory, I believe.  If you'd like to import that axiom 
(not needed for your example, since equality on [nat] is decidable), see 
here:
    https://coq.inria.fr/stdlib/Coq.Logic.Eqdep.html

On 06/08/2015 11:21 AM, Lars Rasmusson wrote:
> Hi,
>
> this might be trivial, but how would one prove this lemma?
>
>     Lemma fobar: eq_refl = mult_n_O 1.
>
> The left side is of type 0 = 0 and the right side is of type 0 = 1 * 0.
>
> Is the left side equal to the right side, or only of coercible types?
>
> As the type eq only has one constructor, shouldn't that make them the 
> same?