[isabelle] x is a special variable

I am an french beginner in Isabelle. I prove (as an exercise) the
following lemma
lemma "â y. P y â P (f a)"
  apply (erule_tac x="f a" in allE)
  apply (assumption)
But why am I obliged to use x in instantiating the quantifier (x = "f a").
If I use y = "f a" to instantiate the quantifier, I have a message "no
such variable in theorem".

email : michel.levy at imag.fr

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.