coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect
Date: Tue, 31 May 2016 07:58:46 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga11.intel.com
Ironport-phdr: 9a23:zzsylRC9npffRkft/hqXUyQJP3N1i/DPJgcQr6AfoPdwSP78pMbcNUDSrc9gkEXOFd2CrakU2qyL7+u5AzVIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nhqbvp9aKOVwArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Ku4zSqUdBzA7OUg04tfqvF/NV0HHsnAbSyAdlgdCKwnD9hDzGJnr5HjUrO14jWOhOsD5UaozQXDqyqZgSBbljG1PYzs4+2Heh8g2l6VWrw67oARXwojIbYXTP/17KPCONegGTHZMC54CHxdKBZmxOtMC

Dear Jonathan,

your 'specific' notation works like a charm - very intuitive to use.

Just it didn't help me to simplify my proof, because my list_mirror lemma is
the wrong way around, and the right one is about as un-elegant to prove as
the prove for the induction scheme I already have. It looks like it has to be
like this.

Thanks & best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Soegtrop, Michael, 05/30/2016
- Re: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Adam Chlipala, 05/30/2016
- Re: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Jonathan Leivent, 05/30/2016
  - RE: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Soegtrop, Michael, 05/30/2016
  - Re: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Tej Chajed, 05/30/2016
  - RE: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Soegtrop, Michael, 05/31/2016
- Re: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Dominique Larchey-Wendling, 05/31/2016
  - Re: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Arnaud Spiwack, 05/31/2016