[STATEMENT]
lemma return_returns_heap [iff]: "(h \<turnstile> return x \<rightarrow>\<^sub>h h') = (h = h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<turnstile> return x \<rightarrow>\<^sub>h h' = (h = h')
[PROOF STEP]
unfolding returns_heap_def return_def execute_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case the_prog (Prog (\<lambda>h. Inr (x, h))) h of Inl x \<Rightarrow> False | Inr (xa, xb) \<Rightarrow> h' = xb) = (h = h')
[PROOF STEP]
by auto