Skip to Content.

Sympa Menu

coq-club - Re: Re: [Coq-Club] Introduce existing variable

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Re: [Coq-Club] Introduce existing variable

chronological Thread

From: Michael<michaelschausten AT googlemail.com>
To: coq-club AT inria.fr
Subject: Re: Re: [Coq-Club] Introduce existing variable
Date: Mon, 19 Jul 2010 11:18:46 +0200

Thanks to both of you, [destruct] was the tactic I was looking for.

[Coq-Club] Introduce existing variable, Michael
- Re: [Coq-Club] Introduce existing variable, Thomas Braibant
- Re: [Coq-Club] Introduce existing variable, Vincent Siles
- <Possible follow-ups>
- Re: Re: [Coq-Club] Introduce existing variable, Michael

Archive powered by MhonArc 2.6.16.