coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] injectivity on existT

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] injectivity on existT
Date: Mon, 30 May 2016 17:48:30 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f176.google.com
Ironport-phdr: 9a23:QxGq8RyHUNR/o27XCy+O+j09IxM/srCxBDY+r6Qd0ewQIJqq85mqBkHD//Il1AaPBtWKra8Yw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2WVTerzWI4CIIHV2nbEwudrWzR9Kapv/0/t7x0qWbWx9Piju5bOE6BzSNhiKViPMrh5B/IL060BrDrygAUe1XwWR1OQDbxE6ktY+YtaRu+CVIuv8n69UIEeCjJ/x5HvRkC2ENNHl9z8n2v1GXRgyWo3AYT28+kxxSAgGD4gusDbnrtS6vlO170TWaNMu+ab01Rzmk8+8/ShjuiSQKMzM02G7Sg810yqlcpUTy9FRE34fIbdTNZ7JFdaTHcIZfHDIZUw==

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?

-- Jonathan

[Coq-Club] injectivity on existT, Jonathan Leivent, 05/30/2016
- Re: [Coq-Club] injectivity on existT, Adam Chlipala, 05/30/2016
  - Re: [Coq-Club] injectivity on existT, Daniel Schepler, 05/31/2016
    - Re: [Coq-Club] injectivity on existT, Jonathan Leivent, 05/31/2016
      - Re: [Coq-Club] injectivity on existT, Jonathan Leivent, 05/31/2016