The Coq mailing list

[Lars Rasmusson <Lars.Rasmusson AT sics.se>]

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?