coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: beginners question

From: "Robert R. Schneck" <schneck AT math.berkeley.edu>
To: <coq-club AT pauillac.inria.fr>
Subject: Re: beginners question
Date: Tue, 9 Oct 2001 08:21:11 -0700 (PDT)

Hello. I just wanted to add that I think "Generalize" provides a good way
to do forward reasoning now. E.g. given

H0: a
H1: a->b
========
b

One can use "Generalize (H1 H0); Intro H2" to obtain

H0: a
H1: a->b
H2: b
========
b

Robert

beginners question, Bauer, Robert
- Re: beginners question, Clement Renard
- Re: beginners question, Hugo Herbelin
  - Re: beginners question, Robert R. Schneck