coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Using apply on a hypothesis with universal quantification

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: Laurent Théry <Laurent.Thery AT inria.fr>, Coq Club <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Using apply on a hypothesis with universal quantification
Date: Thu, 7 Nov 2013 13:03:11 +0000
Accept-language: de-DE, en-US

Dear Laurent,

treating hypothesis as functions definitely opens the door to some new
interesting thoughts, but I am still standing on the doorstep, puzzled ;-)

I guess in this (even more stupid) case:

Example Test2: forall c d:nat, ( forall a b:nat, a = b -> a+a=b+b) -> c = d.
intros c d H.

when I want to leave the a=b untouched and only change the a+a=b+b into
S(a+a)=S(b+b) I cannot apply this technique?

Thanks & best regards,

Michael

[Coq-Club] Using apply on a hypotheis with universal quantification, michael.soegtrop, 11/07/2013
- Re: [Coq-Club] Using apply on a hypotheis with universal quantification, Laurent Théry, 11/07/2013
  - RE: [Coq-Club] Using apply on a hypothesis with universal quantification, Soegtrop, Michael, 11/07/2013
    - Re: [Coq-Club] Using apply on a hypothesis with universal quantification, Laurent Théry, 11/07/2013
      - Re: [Coq-Club] Using apply on a hypothesis with universal quantification, Rui Baptista, 11/07/2013