[STATEMENT]
lemma Var':
  "l V = Some v \<Longrightarrow>
  P,E \<turnstile> \<langle>Var V,(h,l)\<rangle> \<Rightarrow>' \<langle>Val v,(h,l)\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l V = \<lfloor>v\<rfloor> \<Longrightarrow> P,E \<turnstile> \<langle>Var V,(h, l)\<rangle> \<Rightarrow>' \<langle>Val v,(h, l)\<rangle>
[PROOF STEP]
by transfer(rule Var)