Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Is eq_refl = mult_n_O 1 provable?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is eq_refl = mult_n_O 1 provable?


Chronological Thread 
  • From: Lars Rasmusson <Lars.Rasmusson AT sics.se>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Is eq_refl = mult_n_O 1 provable?
  • Date: Mon, 8 Jun 2015 17:21:57 +0200

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?





Archive powered by MHonArc 2.6.18.

Top of Page