coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Injectivity of existT

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Injectivity of existT
Date: Fri, 14 Feb 2020 21:43:11 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chris.dams.nl AT gmail.com; spf=Pass smtp.mailfrom=chris.dams.nl AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f41.google.com
Ironport-phdr: 9a23:UN0gLRVo/Q+prD06ApgNC2UVgzPV8LGtZVwlr6E/grcLSJyIuqrYYxeDt8tkgFKBZ4jH8fUM07OQ7/m8HzNYqs/d6TgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMucQam4lvJro+xhfUrXZEZvldyH91K16Ugxvz6cC88YJ5/S9Nofwh7clAUav7f6Q8U7NVCSktPn426sP2qxTNVBOD6XQAXGoYlBpIGBXF4wrhXpjtqCv6t/Fy1zecMMbrUL07QzWi76NsSB/1lCcKMiMy/W/LhsBsiq9QvRSsrAF9zYHJeoGYLPVxfq3fct0aS2RPXdtfWTJdDY6ndYQDE/AMMPxEo4XhpVYDqwa1Cwm2BOPozz9FnmH73a0g0+QgCgHNwQIuEMgLsHTPsd74M7sdUeCvzKnJ1jXPde5Z1i346IjTaBwhp/WMUKl/ccrU00YvFgfFgk+MpoziOjOYz+IAuHWY4ep4Te+jlXIrpgVrrjWsxsogkJfFipwLxlze+ih13YA4LsCiRkFhe96rCp5QujmaN4RoRsMiRHlluCMgxb0HvZ63ZTUKx446yxLGZfyKfJWE7gjsVOaWJjd4i3Zld6ylixmu9kigz/XwVsiy0FlUsipIisfAumwJ2hDJ6cWKSuFx8lm/1TqRzQze5fxILVgxlaXBKp4hxrAwloAUsUTGBiL5hEX2jLWXdkU/4OSn9v7oYrD9ppOGMY90jhrzMqsrmsOlAOQ4NhICUHSc+eS5zLHj51H2QK1Wjv0qlanUqIzVJcMCpqKgHwBV1psj5A2kAje90NUYmGEHI0hfdBKGiYjpIVDOL+riAfexmVT/2AtskvvBJ/jqBojHZizIl66kdrJg4WZdzhAyxJZR/cQHJKsGJafYWlXwr5T0Bxoie1i/w/zmE5Nx34YFH2SLKqCcOaLW91SP47R8cKG3eIYJtWOleLAe7Pn0gCphwA5PTeySxZISLUuAMLFjKkSdb2Drh45YQ2gPtws6CuftjQ/bCGIBVzOJR6s5owoDJse+F46aH9KihbWA2GGwGZgEPjkbWGDJKm/hcsC/Y9lJaC+WJZU8wDkNVLzkVoZ4kB/y7Un1zL1oKueS8Sod58ru

Besides what Adam Chlipala writes there also is inj_pair2_eq_dec en Eqdep_dec

which does not need any axiom but which needs the assumption that equality on

T is decidable.

inj_pair2_eq_dec
: forall A : Type,
(forall x y : A, {x = y} + {x <> y}) ->
forall (P : A -> Type) (p : A) (x y : P p),
existT P p x = existT P p y -> x = y

[Coq-Club] Injectivity of existT, John Li, 02/14/2020
- Re: [Coq-Club] Injectivity of existT, Adam Chlipala, 02/14/2020
- Re: [Coq-Club] Injectivity of existT, Chris Dams, 02/14/2020
  - Re: [Coq-Club] Injectivity of existT, Cao Qinxiang, 02/15/2020