coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to represent the assumption of a finite set

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Damien Pous <Damien.Pous AT inrialpes.fr>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] how to represent the assumption of a finite set
Date: Fri, 6 May 2011 14:06:20 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=aY6sM1hgbcmsceDyGNujqQXiuq8IpqwCY0Y9tdLn2PGQlhfb/djYSaiQ/ZM18907NZ agLtxD1TNTftJqZZJ2DyymS+VKHoJejy/kWpcPew/1rByp9j8bflVj5e3v3mJ0mK7yxY ynPLjhw75lQmgWGnxaGHVfpXyfZBOONBd3qBo=

2011/5/6 Damien Pous
<Damien.Pous AT inrialpes.fr>:
> Variable U: Set.
> Variable X: list U.
> Goal forall x, In x U -> x = x.
> ...

I guess you meant
Goal forall x, In x X -> x = x.

[Coq-Club] how to represent the assumption of a finite set, Gyesik Lee
- <Possible follow-ups>
- [Coq-Club] how to represent the assumption of a finite set, Gyesik Lee
  - Re: [Coq-Club] how to represent the assumption of a finite set, Vincent
    - Re: [Coq-Club] how to represent the assumption of a finite set, Damien Pous
    - Re: [Coq-Club] how to represent the assumption of a finite set, Damien Pous
      - Re: [Coq-Club] how to represent the assumption of a finite set, Alexandre Pilkiewicz
        
        Re: [Coq-Club] how to represent the assumption of a finite set, AUGER Cedric
  - Re: [Coq-Club] how to represent the assumption of a finite set, Thomas Strathmann
    - Re: [Coq-Club] how to represent the assumption of a finite set, Gyesik Lee