[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)
  done
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
http://membres-liglab.imag.fr/michel.levy 




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