The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

What do you mean "variables are dummy"?

Your statement seems similar to "forall X, P X -> forall Y, P Y" which 
is true iff "forall x, P x"
maybe you meant to parenthesize as "(forall X, P X) -> forall Y, P Y"?

Gaëtan Gilbert

On 01/10/2019 00:14, richard Dapoigny wrote:
> Dear Coq users,
>
> Assuming classical logic, i have the following goal:
>
> ∀ X0 Y0 : N,
>    (eta X0 Balls ∧ eta Y0 Balls ∧ eta B (el X0) ∧ eta X0 (ext A) ∧ eta B 
> (el Y0) ∧ eta Y0 (ext A)  → eta X0 (el Y0) ∨ eta Y0 (el X0))
>    → ∀ X'0 Y'0 : N,
>        eta X'0 Balls ∧ eta Y'0 Balls ∧ eta B (el X'0) ∧ eta X'0 (ext A) 
> ∧ eta B (el Y'0) ∧ eta Y'0 (ext A)  → eta X'0 (el Y'0) ∨ eta Y'0 (el X'0)
>
> since variables are dummy, I expect to solve it with classical tactics 
> such as eauto, tauto, etc. However none of these seems to work. Is 
> anybody has some hints?
>
> Thanks for your help,
>
> Richard
>
> --
> *Richard Dapoigny*
> /Associate Professor/ - LISTIC Laboratory
> University Savoie Mont-Blanc
> 5, chemin de Bellevue
> Po. Box 80439
> Annecy-le-Vieux 74940
> FRANCE
> https://www.listic.univ-smb.fr/en/presentation-en/members/lecturers/richard-dapoigny-en/ 
>
>
> /****** People who don't know history are condemned to repeat it. ******/