coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] cases in leq proof

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] cases in leq proof
Date: Tue, 22 Dec 2020 17:04:08 -0300 (UYT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
Dkim-filter: OpenDKIM Filter v2.9.0 mta04.in.vera.com.uy 0F0AC222E07
Ironport-phdr: 9a23:d3BjxBB4BtFTFtCcKdVmUyQJP3N1i/DPJgcQr6AfoPdwSPTzo8bcNUDSrc9gkEXOFd2Cra4d1KyM6/yrADZdqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5wIRmsswndqsYbjYR/JqovyhbCv2dFdflRyW50P1yYggzy5t23/J5t8iRQv+wu+stdWqjkfKo2UKJVAi0+P286+MPkux/DTRCS5nQHSWUZjgBIAwne4x7kWJr6rzb3ufB82CmeOs32UKw0VDG/5KplVBPklCEKPCM+/2/XjcxwlrlUoBO8qBNi3YHUZoObO+dkfqjAed8XRXZNUtpUWyFHH4iybZYAD/AZMOhWr4fzuVgAohmjCwajGOzvyyNIi2Ts0qEmz+suCh3K0BAmEtkTsHrUttL1NKIKXO6v1qbI0S/Db/JK1jf88ofDbwovru+WXb1qbcrR1U4vHB7Cg1WIsozlJy2a1v4XvGiH8+pgUvmii3A5pAFruDej3Nsjio7Mho4P11DF9Tx0zYAoLtO7UE52ecCoHIdMuy2AOIZ6XtkuTm91tCog17ELtoa3cDUIxZg53RLTdfOKf5KG7x7+TuqcLyt0iXR4c7y/gBay61OvyuzhWcapzllKqChLncTWtn0V2RLd6taJRPh/8Um81jmAywHT6v1fLE8uiabUN4UuzqIsmpYLv0rNHjH4lkb0g6GLeUor5umo6/j8b7r8upOTK5R7hh3iPqkoh8exG/43MhIUUGie4em81KPs/Un+QLhSi/05iKjZsJTAKcQFuKG5GRVa3pw/5Ba4CjeqyskYnHkfIFJEfhKIkZTpNknQLPzkEfuzmVuhnCtxy/3II7HtGIjBI3fbnLfkZ7l96kpcyAQpzdBY4pJZEqkBIOnrWkDvrtzXFAM5MxCzw+v8FtVyyJkeVniVDqCFN6PStEWE5v8vIuWUfo8apC79K+Q55/7plXI2hVgdfbCw0ZQLbHC4A+9pLl6CYXvsh9cBCX0FshA/TOzskl2CUCRca2y8X6ImtXkHD9etCp6GTYSwivTV1yCiW5ZSe2puC1aWEH6ueZ/SCNkWbyfHGsZ9iD0PVLHpc4I73A2ys0eu06F/I/Dd5jEfnYzuztEz7OrW0wwjo28nR/+B2n2AGjgn1lgDQCU7if0n+RUhmGfG6rBxhrljLfIW/+lAC1xoK5PGxqpxDNW0RxOTJo7UGmbjec2vBHQKdvx0w9IKZB8tSdCrjxSFwSewCvkekLnNGY1mqvuNjUi0HN50zjP97IdkilAnRsVVMmj/3fxh+hLaQYXOlgOEhvTzeA==

Is there some way to make a case analisis over a proof

of a leq proposition?

Regards,

Patricia

[Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Adam Chlipala, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
  - Re: [Coq-Club] cases in leq proof, Adam Chlipala, 12/22/2020
    - Re: [Coq-Club] cases in leq proof, Robbert Krebbers, 12/22/2020
    - Re: [Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
      - Re: [Coq-Club] cases in leq proof, Dominique Larchey-Wendling, 12/23/2020
      - Re: [Coq-Club] cases in leq proof, Castéran Pierre, 12/23/2020