coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: Stefan Monnier <monnier+lists.coq/news/ AT rum.cs.yale.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable
Date: Tue, 10 Dec 2002 18:27:25 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Dec 10, 2002 at 12:02:52PM -0500, Stefan Monnier wrote:
> It seems silly, but I can't seem to figure out how to prove

> (iptr r n)=(iptr ?2570 ?2571)

Try:
Lemma xeqx: (A:Set)(x:A)(x=x).
Proof.
Reflexivity.
Qed.

And use "Apply xeqx.". I noticed that kind of things helps with
metavariables.

--
Lionel

[Coq-Club] Instantiating "existential" ?2730 meta-variable, Stefan Monnier
- Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable, Lionel Elie Mamane
  - Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable, Stefan Monnier
    - Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable, Lionel Elie Mamane
      - Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable, Claudio Sacerdoti Coen