# [isabelle] some problems with the /\ quantifier

```I have a certain predicate whose definition is not important for this
question, so assume it is

definition P :: "real â bool"
where "P x = False"

and assume I proved it holds for x's that equal 'real_of_int(y)',

lemma tl1:
fixes x :: real and
y :: int
assumes "x = real_of_int(y)"
shows   "P(x)"
sorry

now I want to prove something equivalent but easier to use,

lemma
fixes        w :: real
assumes "w \<in> Ints"
shows     "P(w)"

I want to use lemma tl1, so I start the proof with

apply (rule_tac q=w in Ints_cases)
apply (rule assms)

after which the goal is

goal (1 subgoal):
1. â z. w = real_of_int z ==> P w

so, the only thing left is to substitute w and z in tl1 :

apply (rule tl1 [of w z])

but this doesn't work as I expected, and I get a new goal with a new
variable za.

goal (1 subgoal):
1. â za. w = real_of_int za ==> w = real_of_int z

what am I doing wrong ?

```

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