coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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?
- [Coq-Club] Is eq_refl = mult_n_O 1 provable?, Lars Rasmusson, 06/08/2015
- Re: [Coq-Club] Is eq_refl = mult_n_O 1 provable?, Adam Chlipala, 06/08/2015
- Re: [Coq-Club] Is eq_refl = mult_n_O 1 provable?, Jonathan Leivent, 06/08/2015
- Re: [Coq-Club] Is eq_refl = mult_n_O 1 provable?, Lars Rasmusson, 06/08/2015
- Re: [Coq-Club] Is eq_refl = mult_n_O 1 provable?, Daniel Schepler, 06/08/2015
- Re: [Coq-Club] Is eq_refl = mult_n_O 1 provable?, Lars Rasmusson, 06/08/2015
- Re: [Coq-Club] Is eq_refl = mult_n_O 1 provable?, Jonathan Leivent, 06/08/2015
- Re: [Coq-Club] Is eq_refl = mult_n_O 1 provable?, Adam Chlipala, 06/08/2015
Archive powered by MHonArc 2.6.18.