coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Injectivity of existT

From: John Li <johnli0135 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Injectivity of existT
Date: Fri, 14 Feb 2020 14:56:28 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=johnli0135 AT gmail.com; spf=Pass smtp.mailfrom=johnli0135 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f48.google.com
Ironport-phdr: 9a23:t9xdrxDIAMOyCFKIHlHrUyQJP3N1i/DPJgcQr6AfoPdwSPryosbcNUDSrc9gkEXOFd2Cra4d16yJ6+u5AjRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRq7oR/Tu8UKjoduN6g8xgfUqXZUZupawn9lKl2Ukxvg/Mm74YRt8z5Xu/Iv9s5AVbv1cqElRrFGDzooLn446tTzuRbMUQWA6H0cUn4LkhVTGAjK8Av6XpbqvSTksOd2xTSXMtf3TbAwXjSi8rtrRRr1gyoJKzI17GfagdF2galGohyuugZ/zpbbb4+VOvRwfb7Tc80GSmdaRMldSzZMD5mgY4cTDecMO/tToYnnp1sJqBuzHQ2iBOTvyj9Om3T426w62PkmHAHE2wwgH9QOsHDVrNnpKasfX+C4wbLHzTXGdfxW2DP95JLUfRAmpPGBRLR9etfSx0k3Dw7JkEmcpIj/Mz6W1ukBqXaX4/ZjWO61hGMqqAd8qSW1yMg2kInGnIcVx0jE9SpnxIY1IsW1SEthbt6lFJtcrj+VOJZrTs87TWFltyU3xqcJuZ68eygKx5AnyADFZ/ObdIiI5wrvVOeXIThmmHJoYKyziwq2/ES6yeDxVtO43EhWoidGiNXBuXMA2wTW6sedS/t9+kmh2SyI1wDW8uxEI0c0lardK54lw748iocfvErDEyLtl0X2ibWZdkQg+uSy9+vnZbDmqoeGN4BokgH+LrgumsunDOskNQgORnGX9vi41L3+5kL0W65Kj/0zkqnBqp/WP8UbpqijAw9UyIkv8Ri/Dy31mOgfyHIANRdOfA+Np4nvIVDHZv7iXtmlhFH5sjBrwbjiP/W1AJLNKHzCyO66IJ5y7kddzEw4ytUJtMEcMa0IPP+mAhy5j9ffFBJsa1XokdaiM81008YlYUzKGrWQafqAvlqB5+ZpKO6JNtdM6WTNbsM97vurtkcX3FoUfK2nx5wSMSnqEfFvIkHfan3p0I5YTDU6+zEmRemvs2WsFD5eY3HoAvA57zA/TY+qVMLNGtDrj7uG0yO2WJZRYzIeBw==

Hi,

I have a proof of the following statement which assumes injectivity of dependent equality:

forall (A : Type) P x y, existT P A x = existT P A y -> x = y.

Is it possible to prove this without using any extra assumptions?

Thanks,
John

[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