The Coq mailing list

[ruy.leywild AT imdea.org]

Hi all, in the following example I want to prove injectivity of a
dependent pair.  Below, inj has an explicit type parameter whereas inj'
assumes the variables have type unit.  In v8.2pl1 both proofs work; but in
higher versions (v8.2pl2, v8.3, and v8.3pl1) the first works but the
latter fails(!).  My current workaround is to use inj to prove inj', but
I'd rather prove it directly if possible.  Any suggestions?

Thanks, Ruy.


Require Import Eqdep.
Set Implicit Arguments.

Record dynamic : Type := dyn {typ : Type; val : typ}.

Lemma inj A (x y : A) : dyn x = dyn y -> x = y.
Proof. intros A x y H; injection H; apply inj_pairT2. Qed.

Lemma inj' (x y : unit) : dyn x = dyn y -> x = y.
Proof. intros x y H; injection H; apply inj_pairT2. Qed.

> intros x y H; injection H; apply inj_pairT2.
>               ^^^^^^^^^^^
Error: Failed to decompose the equality.