Ssreflect Users Discussion List

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
v8.2pl2 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. move=>A x y; case; apply: inj_pairT2. Qed.

Lemma inj' (x y : unit) : dyn x = dyn y -> x = y.
Proof. move=>x y; case; apply: inj_pairT2. Qed.

> Proof. move=>x y; case; apply: inj_pairT2. Qed.
>                   ^^^^
Error: Failed to decompose the equality.