coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Laurent Théry <Laurent.Thery AT inria.fr>
To: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Using apply on a hypothesis with universal quantification
Date: Thu, 07 Nov 2013 14:07:17 +0100

On 11/07/2013 02:03 PM, Soegtrop, Michael wrote:

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 t

You still can but it is more difficult to build blindly ;-)

assert (G := fun a b H1 => (f_equal S (H a b H1))).

[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