coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] help with automating derived UIP_refl proofs
Date: Wed, 31 Aug 2016 23:04:57 -0400
Authentication-results: mail3-smtp-sop.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:esGJjBJrYMa5zdQMPdmcpTZWNBhigK39O0sv0rFitYgUL/vxwZ3uMQTl6Ol3ixeRBMOAuqsC1rKd7PqoGTRZp83Q6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJLL+j4UrTfk96wn7jrvcaCOkMV3HHiO/sydEzw9lSJ8JFOwMNLEeUY8lPxuHxGeuBblytDBGm4uFLC3Pq254Np6C9KuvgspIZqWKT+eLkkH/QDVGx1ezN92Mq+vh7aCACL+3E0U2MMkxMODRKWwgv9W8LTtS3zqup03mG+MMzoQLYoEWCg6KFqSxLshSovODsw8WWRgct12vEI6Cm9rgByltaHKLqeM+BzK/vQ

On 08/31/2016 07:46 PM, Jason Gross wrote:

Here's the pointed version of UIP-respecting-isomorphism:

Thanks, Jason!

-- Jonathan

Re: [Coq-Club] help with automating derived UIP_refl proofs, Dominique Larchey-Wendling, 09/01/2016
- Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 09/01/2016
  - Message not available
    - Re: [Coq-Club] help with automating derived UIP_refl proofs, Jason Gross, 09/01/2016
      - Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 09/01/2016
        
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jason Gross, 09/01/2016
        
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 09/01/2016
        
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 09/01/2016
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jason Gross, 09/01/2016
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jason Gross, 09/01/2016
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 09/01/2016
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jason Gross, 09/02/2016
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Dominique Larchey-Wendling, 09/08/2016