[STATEMENT]
lemma reach2: 
  "\<not> s\<turnstile> l reachable_from x \<Longrightarrow> \<not> s\<langle>l:=y\<rangle>\<turnstile> l reachable_from x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> s\<turnstile> l reachable_from x \<Longrightarrow> \<not> s\<langle>l := y\<rangle>\<turnstile> l reachable_from x
[PROOF STEP]
by (simp)