[STATEMENT]
lemma Methods_into_Methods':
  assumes "Program P \<turnstile> C sees_methods Mm"
  shows "\<exists>Mm'. Methods' P C Mm' \<and> Mm = map_of Mm'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Mm'. Methods' P C Mm' \<and> Mm = map_of Mm'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Program P \<turnstile> C sees_methods Mm

goal (1 subgoal):
 1. \<exists>Mm'. Methods' P C Mm' \<and> Mm = map_of Mm'
[PROOF STEP]
by induct(auto intro: Methods'.intros simp add: map_of_map2 map_add_def)