[STATEMENT]
lemma new_element_get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a: 
  "h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M ptr getter) h h'
[PROOF STEP]
by(auto simp add: new_element_def get_M_defs preserved_def split: prod.splits option.splits 
      elim!: bind_returns_result_E bind_returns_heap_E)