[STATEMENT]
lemma only_touches_opening:
  assumes \<open>only_touches i branch xs\<close> \<open>(v, v') \<in> xs\<close> \<open>branch !. v = Some (ps, a)\<close>
  shows \<open>i = a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
only_touches i branch xs
(v, v') \<in> xs
branch !. v = Some (ps, a)

goal (1 subgoal):
 1. i = a
[PROOF STEP]
unfolding only_touches_def is_at_def
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>xs. \<forall>ps a. branch !. v = Some (ps, a) \<longrightarrow> i = a
(v, v') \<in> xs
branch !. v = Some (ps, a)

goal (1 subgoal):
 1. i = a
[PROOF STEP]
by auto