coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] aren't (x = n -> y = n) and (x = y) the same thing?

From: Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>
To: coq-club AT inria.fr
Cc: sedrikov AT gmail.com
Subject: Re: [Coq-Club] aren't (x = n -> y = n) and (x = y) the same thing?
Date: Wed, 11 Jun 2014 07:42:01 +0200

Hi Cedric,

> When you perform some induction, you sometimes need to generalize your goal.

This is interesting. Could you state a simple (if possible, "simplest")
example goal where this happens?

Thanks!
Best regards,

Bruno

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail

[Coq-Club] aren't (x = n -> y = n) and (x = y) the same thing?, Mathijs Kwik, 06/08/2014
- Re: [Coq-Club] aren't (x = n -> y = n) and (x = y) the same thing?, Cedric Auger, 06/09/2014
  - Re: [Coq-Club] aren't (x = n -> y = n) and (x = y) the same thing?, Mathijs Kwik, 06/10/2014
- <Possible follow-up(s)>
- Re: [Coq-Club] aren't (x = n -> y = n) and (x = y) the same thing?, Bruno Woltzenlogel Paleo, 06/11/2014
  - Re: [Coq-Club] aren't (x = n -> y = n) and (x = y) the same thing?, Cedric Auger, 06/11/2014
  - Re: [Coq-Club] aren't (x = n -> y = n) and (x = y) the same thing?, Cody Roux, 06/11/2014