[STATEMENT]
lemma boxed_i_ex:
  assumes "wfI T \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "wfTh T"
  shows  "\<exists>i'. T ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i'.  T  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 T ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. \<exists>i'.  T  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
[PROOF STEP]
proof(induct \<Gamma> arbitrary: i rule:\<Gamma>_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk> T ; GNil[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T GNil b bv i)
 2. \<And>x ba c \<Gamma>' i. \<lbrakk>\<And>i. \<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T \<Gamma>' b bv i);  T ; ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>') b bv i)
[PROOF STEP]
case GNil
[PROOF STATE]
proof (state)
this:
 T ; GNil[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T

goal (2 subgoals):
 1. \<And>i. \<lbrakk> T ; GNil[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T GNil b bv i)
 2. \<And>x ba c \<Gamma>' i. \<lbrakk>\<And>i. \<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T \<Gamma>' b bv i);  T ; ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>') b bv i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 T ; GNil[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 T ; GNil[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. \<exists>a.  T  ; GNil ; b , bv \<turnstile> i \<approx> a
[PROOF STEP]
using boxed_i_GNilI
[PROOF STATE]
proof (prove)
using this:
 T ; GNil[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T
 ?\<Theta>  ; GNil ; ?b , ?bv \<turnstile> ?i \<approx> ?i

goal (1 subgoal):
 1. \<exists>a.  T  ; GNil ; b , bv \<turnstile> i \<approx> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  ; GNil ; b , bv \<turnstile> i \<approx> a

goal (1 subgoal):
 1. \<And>x ba c \<Gamma>' i. \<lbrakk>\<And>i. \<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T \<Gamma>' b bv i);  T ; ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>') b bv i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x ba c \<Gamma>' i. \<lbrakk>\<And>i. \<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T \<Gamma>' b bv i);  T ; ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>') b bv i)
[PROOF STEP]
case (GCons x' b' c' \<Gamma>')
[PROOF STATE]
proof (state)
this:
\<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  ; \<Gamma>' ; b , bv \<turnstile> ?i \<approx> a
 T ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. \<And>x ba c \<Gamma>' i. \<lbrakk>\<And>i. \<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T \<Gamma>' b bv i);  T ; ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>') b bv i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  ; \<Gamma>' ; b , bv \<turnstile> ?i \<approx> a
 T ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T
[PROOF STEP]
obtain s where 1:"Some s = i x' \<and> wfRCV T s b'[bv::=b]\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  ; \<Gamma>' ; b , bv \<turnstile> ?i \<approx> a
 T ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. (\<And>s. Some s = i x' \<and>  T  \<turnstile> s : b'[bv::=b]\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfI_def subst_gb.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  ; \<Gamma>' ; b , bv \<turnstile> ?i \<approx> a
 T ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
GNil[?uu::=?uv]\<^sub>\<Gamma>\<^sub>b = GNil
((?y, ?b', ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?bv::=?b]\<^sub>\<Gamma>\<^sub>b = (?y, ?b'[?bv::=?b]\<^sub>b\<^sub>b, ?c[?bv::=?b]\<^sub>c\<^sub>b) #\<^sub>\<Gamma> ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1. (\<And>s. Some s = i x' \<and>  T  \<turnstile> s : b'[bv::=b]\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some s = i x' \<and>  T  \<turnstile> s : b'[bv::=b]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. \<And>x ba c \<Gamma>' i. \<lbrakk>\<And>i. \<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T \<Gamma>' b bv i);  T ; ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>') b bv i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some s = i x' \<and>  T  \<turnstile> s : b'[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
obtain s' where 2: "boxed_b T s b' bv b s'"
[PROOF STATE]
proof (prove)
using this:
Some s = i x' \<and>  T  \<turnstile> s : b'[bv::=b]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. (\<And>s'.  T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using boxed_b_ex GCons
[PROOF STATE]
proof (prove)
using this:
Some s = i x' \<and>  T  \<turnstile> s : b'[bv::=b]\<^sub>b\<^sub>b
\<lbrakk> ?T  \<turnstile> ?s : ?b[?bv::=?b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f ?T \<rbrakk> \<Longrightarrow> \<exists>s'.  ?T  \<turnstile> ?s ~ ?b [ ?bv ::= ?b' ] \<setminus> s'
\<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  ; \<Gamma>' ; b , bv \<turnstile> ?i \<approx> a
 T ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. (\<And>s'.  T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'

goal (1 subgoal):
 1. \<And>x ba c \<Gamma>' i. \<lbrakk>\<And>i. \<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T \<Gamma>' b bv i);  T ; ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>') b bv i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'
[PROOF STEP]
obtain i' where 3: "boxed_i T \<Gamma>' b bv i  i'"
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'

goal (1 subgoal):
 1. (\<And>i'.  T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GCons wfI_def subst_gb.simps
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'
\<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  ; \<Gamma>' ; b , bv \<turnstile> ?i \<approx> a
 T ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
GNil[?uu::=?uv]\<^sub>\<Gamma>\<^sub>b = GNil
((?y, ?b', ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?bv::=?b]\<^sub>\<Gamma>\<^sub>b = (?y, ?b'[?bv::=?b]\<^sub>b\<^sub>b, ?c[?bv::=?b]\<^sub>c\<^sub>b) #\<^sub>\<Gamma> ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1. (\<And>i'.  T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
 T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1. \<And>x ba c \<Gamma>' i. \<lbrakk>\<And>i. \<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T \<Gamma>' b bv i);  T ; ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>') b bv i)
[PROOF STEP]
have "boxed_i T ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') b bv i  (i'(x' \<mapsto> s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  ; (x', b', c') #\<^sub>\<Gamma> \<Gamma>' ; b , bv \<turnstile> i \<approx> i'(x' \<mapsto> s')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Some ?s = i x'
 2.  T  \<turnstile> ?s ~ b' [ bv ::= b ] \<setminus> s'
 3.  T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i'
[PROOF STEP]
show "Some s = i x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some s = i x'
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
Some s = i x' \<and>  T  \<turnstile> s : b'[bv::=b]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. Some s = i x'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some s = i x'

goal (2 subgoals):
 1.  T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'
 2.  T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i'
[PROOF STEP]
show "boxed_b T s b' bv b s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'

goal (1 subgoal):
 1.  T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> s ~ b' [ bv ::= b ] \<setminus> s'

goal (1 subgoal):
 1.  T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i'
[PROOF STEP]
show "T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i'
[PROOF STEP]
using  "3"
[PROOF STATE]
proof (prove)
using this:
 T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1.  T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 T  ; \<Gamma>' ; b , bv \<turnstile> i \<approx> i'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 T  ; (x', b', c') #\<^sub>\<Gamma> \<Gamma>' ; b , bv \<turnstile> i \<approx> i'(x' \<mapsto> s')

goal (1 subgoal):
 1. \<And>x ba c \<Gamma>' i. \<lbrakk>\<And>i. \<lbrakk> T ; \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T \<Gamma>' b bv i);  T ; ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_i T ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>') b bv i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
 T  ; (x', b', c') #\<^sub>\<Gamma> \<Gamma>' ; b , bv \<turnstile> i \<approx> i'(x' \<mapsto> s')

goal (1 subgoal):
 1. \<exists>a.  T  ; (x', b', c') #\<^sub>\<Gamma> \<Gamma>' ; b , bv \<turnstile> i \<approx> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  ; (x', b', c') #\<^sub>\<Gamma> \<Gamma>' ; b , bv \<turnstile> i \<approx> a

goal:
No subgoals!
[PROOF STEP]
qed