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: AUGER Cedric <Cedric.Auger AT lri.fr>
To: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
Cc: Damien Pous <Damien.Pous AT inrialpes.fr>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] how to represent the assumption of a finite set
Date: Sun, 8 May 2011 13:09:22 +0200

Le Fri, 6 May 2011 14:06:20 +0200,
Alexandre Pilkiewicz
<alexandre.pilkiewicz AT polytechnique.org>
a écrit :

> 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.

In fact "∀ x, In x X → x = x" is not very informative either ;) (but
type-checks)

[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