# [isabelle] Instantiation problem

Hello everybody,
during a proof I have obtained:
(getPc (stof (snd s)) ! (cinc i) = S) /\ getDir (stof (snd s)) ! (cinc i) =
right /\ getPc (stof (snd s)) ! i = ER
where (cinc i)::nat.
Now I want demonstrate the goal:
EX i::nat. ((getPc (stof (snd s)) ! i = S) /\ getDir (stof (snd s)) ! i =
right /\ getPc (stof (snd s)) ! cdec i = ER)
It follow from a simple instantiation ( i <-- (cinc i) ) but I don't find
how to help Isabelle to execute it and using normal proof methods Isabelle
don't find the solution.
Can you help me?
Sorry, I know that this is a very trivial problem but I don't understand it.
Thanks
Gabriele

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