The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Mon, Nov 21, 2005 at 10:30:15AM +0800, Li Long wrote:

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

Well, just write it like that:

forall ( T : Set )( A : Prop ), ( forall x : T, A ) -> A.

A cannot have _any_ free variables, thus also not x. But I don't think
you'll be able to prove that; you'd need T to be non-empty. Something
provable would be:

forall ( T : Set )( A : Prop ), T -> ( forall x : T, A ) -> A.


-- 
Lionel