The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/30/2016 06:45 PM, Daniel Schepler wrote:
> On Mon, May 30, 2016 at 2:50 PM, Adam Chlipala 
> <adamc AT csail.mit.edu>
>  wrote:
> > In general, it requires an axiom.  If you [Require Import Eqdep], you get it
> > as [inj_pair2].
> >
> >
> > On 05/30/2016 05:48 PM, Jonathan Leivent wrote:
> > > Is this provable?:
> > >
> > > Lemma existT_inj : forall T f x a b, @existT T f x a = @existT T f x b ->
> > > a = b.
> > >
> > > I can't prove it with injectivity, or by f_equal with projT2.  If it is
> > > provable, what's the secret ingredient?
> And in a specific case, if you have a decision procedure for equality
> to x, then existT_inj holds for that case.  (Ex: if T = nat; or if T =
> option A, and x = None.)

That's precisely what I need - as I do have decidable equality for the 
type involved.  I see it now: Eqdep_dec.inj_pair2_eq_dec:

Thanks!

-- Jonathan