coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] injectivity of constructors

From: Lily Chung <ikdc AT mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] injectivity of constructors
Date: Thu, 13 Dec 2018 19:53:34 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ikdc AT mit.edu; spf=Pass smtp.mailfrom=ikdc AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-2.mit.edu
Importance: Normal
Ironport-phdr: 9a23:dzYm/hJsA8Yes7mHQtmcpTZWNBhigK39O0sv0rFitYgQLfXxwZ3uMQTl6Ol3ixeRBMOHs6IC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwZFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhikaOTA68m7ZitJ+g6FBrh2gqBNw34HabZqVNPVlZK7RYc8WSXZDU8tXSidPApm8b4wKD+cZO+hYro39plsTphagBQmsGeXvyjBVjXLx3K060PkuHh3d0QwlHtIOrG7Yo8voO6cPSO24yrTDwzbbb/5OxDvw65LEfxQ7rf2SXb98a9fdxEc3Gw/YjFict5bpMjOU2+gXrWSW4fBsWOKhhmMhtgp/uCKgxt02hYnMno8Vyk7L9SF+wIstONK4TU96bcehEJRKtiGaM5B2Td0+TG1xoyY11qcJuZi9fCcU0pQr3gDTZ+aCc4iJ/hLvTvieLiplhH59ebK/gQi98VS4x+HhVcS4ylJHojBbntTMrHwByhLe5tCCSvRn/0eh3TiP1xrU6uFBOU00lKnbJIM9zbMrk5oTsFjDEjXol0rrka+abl8k9fSw6+T7frXmoYeROJNzigHnK6ghhsi/AfkjPQUVRGia+eG81KX58kHjQbVKiOc2kqjDv5zAK8QbvP3xPwgA2YE6rh27Ej2O0dICnHBBIkgWVgiAit3NOlXfaNv4EPGwywCtkztg7/XHIvvsDoibfSuLq6voYbsosx0U8wE0190Kv8sFWIFEG+r6XwrKjPKdCxY4NwKuxOO2WtB8ysUTVX/dW/bFYpOXikeB46cUG8fJfJUc6WT4KuRj6vLz3ydgxA0tOJKx1J5SU0iWW/RrJ0LCOCjgh8VEFG4LuhEzR6nxg1SEVzNJIiz0WqMgoDw3FdD+AA==

That follows from general properties of equality, and has nothing to do with constructors. Try f_equal.

[Coq-Club] injectivity of constructors, Jeremy Dawson, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Pierre Courtieu, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Lily Chung, 12/14/2018
  - Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
    - Re: [Coq-Club] injectivity of constructors, Jeremy Dawson, 12/14/2018
      - Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
        
        Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
      - Re: [Coq-Club] injectivity of constructors, Dominique Larchey-Wendling, 12/14/2018
        
        Re: [Coq-Club] injectivity of constructors, Pierre Courtieu, 12/14/2018
        
        Re: [Coq-Club] injectivity of constructors, Lily Chung, 12/14/2018
        
        Re: [Coq-Club] injectivity of constructors, Elazar, 12/14/2018
        RE: [Coq-Club] injectivity of constructors, Jason -Zhong Sheng- Hu, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Jay Kruer, 12/14/2018