coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Help proving

From: Li Long <liwisster AT gmail.com>
To: COQ-CLUB <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] Help proving
Date: Mon, 21 Nov 2005 10:30:15 +0800
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type; b=tLVLjLz+LlfTqXoMl1xdaO3pZhhYupP6wLatRNm3uD+sn4wC5moclPgtUOjLwgNdKeQ+zciiLakME+Qr7on8GciNv9SzMTW3DZNCTwYhS3g+ai5u7S93SNmHY+/VAax/Y8nQzlzBC5mWgks04N0mru8oXW3rXsBhv0Oq/3a3Foc=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

I have been disturbed when I try to prove the following lemma in Coq :
forall ( T : Set )( A : Prop ), ( forall x : T, (* x is not a free variable of A*) A ) -> A.

I have no idea how to formalize the " x is not a free variable of A" in Coq.

Suggestions or alternative solutions are welcome.

Thanks.

[Coq-Club] Help proving, Li Long
- Re: [Coq-Club] Help proving, Lionel Elie Mamane
  - Re: [Coq-Club] Help proving, roconnor
  - Re: [Coq-Club] Help proving, Li Long
    - Re: [Coq-Club] Help proving, Pierre Casteran
      - Re: [Coq-Club] Help proving, Lionel Elie Mamane
        
        Re: [Coq-Club] Help proving, Li Long
        
        Re: [Coq-Club] Help proving, Pierre Casteran
        
        Re: [Coq-Club] Help proving, G�rard Huet
    - Re: [Coq-Club] Help proving, Bruno Barras