[STATEMENT]
lemma b_e_type_get_local:
  assumes "\<C> \<turnstile> [e] : (ts _> ts')"
          "e = Get_local i"
  shows "\<exists>t. ts' = ts@[t] \<and> (local \<C>)!i = t" "i < length(local \<C>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. ts' = ts @ [t] \<and> local \<C> ! i = t &&& i < length (local \<C>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<C> \<turnstile> [e] : ts _> ts'
e = Get_local i

goal (1 subgoal):
 1. \<exists>t. ts' = ts @ [t] \<and> local \<C> ! i = t &&& i < length (local \<C>)
[PROOF STEP]
by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)