The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

Oops... My bad. I didn't realize JMeq_rect had been tampered with.

On Mon, Oct 21, 2013 at 1:53 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 10/20/2013 08:50 PM, Rui Baptista wrote:

I'm confused. Why does it say it can't be proved in chapter "Reasoning About Equality Proofs" of "Certified Programming with Dependent Types".

Require Import JMeq.

Definition jmeq_eq : forall (t1 : Type) (x1 x2 : t1), JMeq x1 x2 -> x1 = x2.
Proof.
refine (fun t1 x1 => _).
refine (JMeq_rect _ _).
refine eq_refl.
Defined.

Try running [Print Assumptions] on some of your definitions.  Even this first one is already depending on the axiom [JMeq_eq], which is used to define [JMeq_rect].