[STATEMENT]
lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK \<phi>\<^sub>m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_types E 3 (Suc (Suc (Suc 0))) (map OK \<phi>\<^sub>m)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_types E 3 (Suc (Suc (Suc 0))) (map OK \<phi>\<^sub>m)
[PROOF STEP]
by (auto simp add: check_types_def phi_makelist_def JVM_states_unfold)