[STATEMENT]
lemma get_set[simp]: "bind get set = return ()"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get \<bind> local.set = return ()
[PROOF STEP]
unfolding bind_def get_def set_def return_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State (\<lambda>s. case run_state (State (\<lambda>s. (s, s))) s of (a, x) \<Rightarrow> run_state (State (\<lambda>_. ((), a))) x) = State (Pair ())
[PROOF STEP]
by simp