[STATEMENT]
lemma boxed_b_ex:
  assumes "wfRCV T s b[bv::=b']\<^sub>b\<^sub>b" and "wfTh T"
  shows "\<exists>s'. boxed_b T s b bv b' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s'.  T  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> s : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. \<exists>s'.  T  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
proof(nominal_induct s arbitrary: b rule: rcl_val.strong_induct)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SBitvec x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBitvec x) b bv b')
 2. \<And>x b. \<lbrakk> T  \<turnstile> SNum x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SNum x) b bv b')
 3. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 4. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 5. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 6. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 7. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 8. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
case (SBitvec x)
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SBitvec x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (8 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SBitvec x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBitvec x) b bv b')
 2. \<And>x b. \<lbrakk> T  \<turnstile> SNum x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SNum x) b bv b')
 3. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 4. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 5. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 6. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 7. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 8. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
have *:"b[bv::=b']\<^sub>b\<^sub>b = B_bitvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = B_bitvec
[PROOF STEP]
using wfRCV_elims(9)[OF SBitvec(1)]
[PROOF STATE]
proof (prove)
using this:
(b[bv::=b']\<^sub>b\<^sub>b = B_bitvec \<Longrightarrow> ?Pa) \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = B_bitvec
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b[bv::=b']\<^sub>b\<^sub>b = B_bitvec

goal (8 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SBitvec x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBitvec x) b bv b')
 2. \<And>x b. \<lbrakk> T  \<turnstile> SNum x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SNum x) b bv b')
 3. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 4. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 5. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 6. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 7. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 8. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
proof (cases "b = B_var bv")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "T  \<turnstile> SBitvec x : B_bitvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> SBitvec x : B_bitvec
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1.  T  \<turnstile> SBitvec x : B_bitvec
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SBitvec x : B_bitvec

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SBitvec x : B_bitvec

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b' = B_bitvec"
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SBitvec x : B_bitvec

goal (1 subgoal):
 1. b' = B_bitvec
[PROOF STEP]
using True SBitvec subst_bb.simps *
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SBitvec x : B_bitvec
b = B_var bv
 T  \<turnstile> SBitvec x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
(B_var ?bv2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = (if ?bv1.0 = ?bv2.0 then ?b else B_var ?bv2.0)
B_int[?bv1.0::=?b]\<^sub>b\<^sub>b = B_int
B_bool[?bv1.0::=?b]\<^sub>b\<^sub>b = B_bool
(B_id ?s)[?bv1.0::=?b]\<^sub>b\<^sub>b = B_id ?s
[ ?b1.0 , ?b2.0 ]\<^sup>b[?bv1.0::=?b]\<^sub>b\<^sub>b = [ ?b1.0[?bv1.0::=?b]\<^sub>b\<^sub>b , ?b2.0[?bv1.0::=?b]\<^sub>b\<^sub>b ]\<^sup>b
B_unit[?bv1.0::=?b]\<^sub>b\<^sub>b = B_unit
B_bitvec[?bv1.0::=?b]\<^sub>b\<^sub>b = B_bitvec
(B_app ?s ?b2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = B_app ?s ?b2.0[?bv1.0::=?b]\<^sub>b\<^sub>b
b[bv::=b']\<^sub>b\<^sub>b = B_bitvec

goal (1 subgoal):
 1. b' = B_bitvec
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b' = B_bitvec

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b = B_var bv
 T  \<turnstile> SBitvec x : B_bitvec
b' = B_bitvec
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SBitvec x : B_bitvec
b' = B_bitvec

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using boxed_b.intros  wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SBitvec x : B_bitvec
b' = B_bitvec
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
\<lbrakk>?bv \<noteq> ?bv';  ?P  \<turnstile> ?s : B_var ?bv'\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_int \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_int [ ?uu ::= ?uv ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_bool \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bool [ ?uw ::= ?ux ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_unit \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_unit [ ?uy ::= ?uz ] \<setminus> ?s
\<lbrakk> ?P  \<turnstile> ?s1.0 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> ?s1' ;  ?P  \<turnstile> ?s2.0 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> ?s2' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> SPair ?s1' ?s2'
\<lbrakk>AF_typedef ?tyid ?dclist \<in> set ?P; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SCons ?tyid ?dc ?s1.0 ~ B_id ?tyid [ ?bv ::= ?b' ] \<setminus> SCons ?tyid ?dc ?s1'
\<lbrakk>AF_typedef_poly ?tyid ?bva ?dclist \<in> set ?P; atom ?bva \<sharp> (?b1.0, ?bv, ?b', ?s1.0, ?s1'); (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b[?bva::=?b1.0]\<^sub>b\<^sub>b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SConsp ?tyid ?dc ?b1.0[?bv::=?b']\<^sub>b\<^sub>b ?s1.0 ~ B_app ?tyid ?b1.0 [ ?bv ::= ?b' ] \<setminus> SConsp ?tyid ?dc ?b1.0 ?s1'
 ?P  \<turnstile> ?s : B_bitvec \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b = B_bitvec"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b = B_bitvec
[PROOF STEP]
using subst_bb_inject *
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_int\<rbrakk> \<Longrightarrow> ?b2.0 = B_int
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_bool\<rbrakk> \<Longrightarrow> ?b2.0 = B_bool
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_unit\<rbrakk> \<Longrightarrow> ?b2.0 = B_unit
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_bitvec\<rbrakk> \<Longrightarrow> ?b2.0 = B_bitvec
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = [ ?b11.0 , ?b12.0 ]\<^sup>b\<rbrakk> \<Longrightarrow> \<exists>b11' b12'. ?b11.0 = b11'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b12.0 = b12'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b2.0 = [ b11' , b12' ]\<^sup>b
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_var ?bv'\<rbrakk> \<Longrightarrow> ?b2.0 = B_var ?bv'
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_id ?tyid\<rbrakk> \<Longrightarrow> ?b2.0 = B_id ?tyid
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_app ?tyid ?b11.0\<rbrakk> \<Longrightarrow> \<exists>b11'. ?b11.0 = b11'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b2.0 = B_app ?tyid b11'
b[bv::=b']\<^sub>b\<^sub>b = B_bitvec

goal (1 subgoal):
 1. b = B_bitvec
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b = B_bitvec

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = B_bitvec
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_bitvec

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using * SBitvec boxed_b.intros
[PROOF STATE]
proof (prove)
using this:
b = B_bitvec
b[bv::=b']\<^sub>b\<^sub>b = B_bitvec
 T  \<turnstile> SBitvec x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
\<lbrakk>?bv \<noteq> ?bv';  ?P  \<turnstile> ?s : B_var ?bv'\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_int \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_int [ ?uu ::= ?uv ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_bool \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bool [ ?uw ::= ?ux ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_unit \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_unit [ ?uy ::= ?uz ] \<setminus> ?s
\<lbrakk> ?P  \<turnstile> ?s1.0 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> ?s1' ;  ?P  \<turnstile> ?s2.0 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> ?s2' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> SPair ?s1' ?s2'
\<lbrakk>AF_typedef ?tyid ?dclist \<in> set ?P; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SCons ?tyid ?dc ?s1.0 ~ B_id ?tyid [ ?bv ::= ?b' ] \<setminus> SCons ?tyid ?dc ?s1'
\<lbrakk>AF_typedef_poly ?tyid ?bva ?dclist \<in> set ?P; atom ?bva \<sharp> (?b1.0, ?bv, ?b', ?s1.0, ?s1'); (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b[?bva::=?b1.0]\<^sub>b\<^sub>b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SConsp ?tyid ?dc ?b1.0[?bv::=?b']\<^sub>b\<^sub>b ?s1.0 ~ B_app ?tyid ?b1.0 [ ?bv ::= ?b' ] \<setminus> SConsp ?tyid ?dc ?b1.0 ?s1'
 ?P  \<turnstile> ?s : B_bitvec \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SBitvec x ~ b [ bv ::= b' ] \<setminus> a

goal (7 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SNum x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SNum x) b bv b')
 2. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 3. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 4. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 5. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 6. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 7. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SNum x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SNum x) b bv b')
 2. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 3. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 4. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 5. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 6. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 7. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
case (SNum x)
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SNum x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (7 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SNum x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SNum x) b bv b')
 2. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 3. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 4. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 5. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 6. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 7. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
have *:"b[bv::=b']\<^sub>b\<^sub>b = B_int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = B_int
[PROOF STEP]
using wfRCV_elims(10)[OF SNum(1)]
[PROOF STATE]
proof (prove)
using this:
(b[bv::=b']\<^sub>b\<^sub>b = B_int \<Longrightarrow> ?Pa) \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = B_int
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b[bv::=b']\<^sub>b\<^sub>b = B_int

goal (7 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SNum x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SNum x) b bv b')
 2. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 3. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 4. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 5. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 6. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 7. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
proof (cases "b = B_var bv")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "T  \<turnstile> SNum x : B_int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> SNum x : B_int
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1.  T  \<turnstile> SNum x : B_int
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SNum x : B_int

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SNum x : B_int

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b' = B_int"
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SNum x : B_int

goal (1 subgoal):
 1. b' = B_int
[PROOF STEP]
using True SNum subst_bb.simps(1) *
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SNum x : B_int
b = B_var bv
 T  \<turnstile> SNum x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
(B_var ?bv2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = (if ?bv1.0 = ?bv2.0 then ?b else B_var ?bv2.0)
b[bv::=b']\<^sub>b\<^sub>b = B_int

goal (1 subgoal):
 1. b' = B_int
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b' = B_int

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b = B_var bv
 T  \<turnstile> SNum x : B_int
b' = B_int
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SNum x : B_int
b' = B_int

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using boxed_b_BVar1I  wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SNum x : B_int
b' = B_int
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b = B_int"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b = B_int
[PROOF STEP]
using subst_bb_inject(1) *
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_int\<rbrakk> \<Longrightarrow> ?b2.0 = B_int
b[bv::=b']\<^sub>b\<^sub>b = B_int

goal (1 subgoal):
 1. b = B_int
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b = B_int

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = B_int
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_int

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using * SNum boxed_b_BIntI
[PROOF STATE]
proof (prove)
using this:
b = B_int
b[bv::=b']\<^sub>b\<^sub>b = B_int
 T  \<turnstile> SNum x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
 ?P  \<turnstile> ?s : B_int \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_int [ ?uu ::= ?uv ] \<setminus> ?s

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SNum x ~ b [ bv ::= b' ] \<setminus> a

goal (6 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 3. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 4. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 5. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 6. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 3. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 4. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 5. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 6. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
case (SBool x)
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (6 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 3. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 4. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 5. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 6. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
have *:"b[bv::=b']\<^sub>b\<^sub>b = B_bool"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = B_bool
[PROOF STEP]
using wfRCV_elims(11)[OF SBool(1)]
[PROOF STATE]
proof (prove)
using this:
(b[bv::=b']\<^sub>b\<^sub>b = B_bool \<Longrightarrow> ?Pa) \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = B_bool
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b[bv::=b']\<^sub>b\<^sub>b = B_bool

goal (6 subgoals):
 1. \<And>x b. \<lbrakk> T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SBool x) b bv b')
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 3. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 4. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 5. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 6. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
proof (cases "b = B_var bv")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "T  \<turnstile> SBool x : B_bool"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> SBool x : B_bool
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1.  T  \<turnstile> SBool x : B_bool
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SBool x : B_bool

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SBool x : B_bool

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b' = B_bool"
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SBool x : B_bool

goal (1 subgoal):
 1. b' = B_bool
[PROOF STEP]
using True SBool subst_bb.simps *
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SBool x : B_bool
b = B_var bv
 T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
(B_var ?bv2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = (if ?bv1.0 = ?bv2.0 then ?b else B_var ?bv2.0)
B_int[?bv1.0::=?b]\<^sub>b\<^sub>b = B_int
B_bool[?bv1.0::=?b]\<^sub>b\<^sub>b = B_bool
(B_id ?s)[?bv1.0::=?b]\<^sub>b\<^sub>b = B_id ?s
[ ?b1.0 , ?b2.0 ]\<^sup>b[?bv1.0::=?b]\<^sub>b\<^sub>b = [ ?b1.0[?bv1.0::=?b]\<^sub>b\<^sub>b , ?b2.0[?bv1.0::=?b]\<^sub>b\<^sub>b ]\<^sup>b
B_unit[?bv1.0::=?b]\<^sub>b\<^sub>b = B_unit
B_bitvec[?bv1.0::=?b]\<^sub>b\<^sub>b = B_bitvec
(B_app ?s ?b2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = B_app ?s ?b2.0[?bv1.0::=?b]\<^sub>b\<^sub>b
b[bv::=b']\<^sub>b\<^sub>b = B_bool

goal (1 subgoal):
 1. b' = B_bool
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b' = B_bool

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b = B_var bv
 T  \<turnstile> SBool x : B_bool
b' = B_bool
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SBool x : B_bool
b' = B_bool

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using boxed_b.intros  wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SBool x : B_bool
b' = B_bool
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
\<lbrakk>?bv \<noteq> ?bv';  ?P  \<turnstile> ?s : B_var ?bv'\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_int \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_int [ ?uu ::= ?uv ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_bool \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bool [ ?uw ::= ?ux ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_unit \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_unit [ ?uy ::= ?uz ] \<setminus> ?s
\<lbrakk> ?P  \<turnstile> ?s1.0 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> ?s1' ;  ?P  \<turnstile> ?s2.0 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> ?s2' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> SPair ?s1' ?s2'
\<lbrakk>AF_typedef ?tyid ?dclist \<in> set ?P; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SCons ?tyid ?dc ?s1.0 ~ B_id ?tyid [ ?bv ::= ?b' ] \<setminus> SCons ?tyid ?dc ?s1'
\<lbrakk>AF_typedef_poly ?tyid ?bva ?dclist \<in> set ?P; atom ?bva \<sharp> (?b1.0, ?bv, ?b', ?s1.0, ?s1'); (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b[?bva::=?b1.0]\<^sub>b\<^sub>b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SConsp ?tyid ?dc ?b1.0[?bv::=?b']\<^sub>b\<^sub>b ?s1.0 ~ B_app ?tyid ?b1.0 [ ?bv ::= ?b' ] \<setminus> SConsp ?tyid ?dc ?b1.0 ?s1'
 ?P  \<turnstile> ?s : B_bitvec \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b = B_bool"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b = B_bool
[PROOF STEP]
using subst_bb_inject *
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_int\<rbrakk> \<Longrightarrow> ?b2.0 = B_int
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_bool\<rbrakk> \<Longrightarrow> ?b2.0 = B_bool
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_unit\<rbrakk> \<Longrightarrow> ?b2.0 = B_unit
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_bitvec\<rbrakk> \<Longrightarrow> ?b2.0 = B_bitvec
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = [ ?b11.0 , ?b12.0 ]\<^sup>b\<rbrakk> \<Longrightarrow> \<exists>b11' b12'. ?b11.0 = b11'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b12.0 = b12'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b2.0 = [ b11' , b12' ]\<^sup>b
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_var ?bv'\<rbrakk> \<Longrightarrow> ?b2.0 = B_var ?bv'
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_id ?tyid\<rbrakk> \<Longrightarrow> ?b2.0 = B_id ?tyid
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_app ?tyid ?b11.0\<rbrakk> \<Longrightarrow> \<exists>b11'. ?b11.0 = b11'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b2.0 = B_app ?tyid b11'
b[bv::=b']\<^sub>b\<^sub>b = B_bool

goal (1 subgoal):
 1. b = B_bool
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b = B_bool

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = B_bool
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_bool

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using * SBool boxed_b.intros
[PROOF STATE]
proof (prove)
using this:
b = B_bool
b[bv::=b']\<^sub>b\<^sub>b = B_bool
 T  \<turnstile> SBool x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
\<lbrakk>?bv \<noteq> ?bv';  ?P  \<turnstile> ?s : B_var ?bv'\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_int \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_int [ ?uu ::= ?uv ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_bool \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bool [ ?uw ::= ?ux ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_unit \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_unit [ ?uy ::= ?uz ] \<setminus> ?s
\<lbrakk> ?P  \<turnstile> ?s1.0 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> ?s1' ;  ?P  \<turnstile> ?s2.0 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> ?s2' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> SPair ?s1' ?s2'
\<lbrakk>AF_typedef ?tyid ?dclist \<in> set ?P; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SCons ?tyid ?dc ?s1.0 ~ B_id ?tyid [ ?bv ::= ?b' ] \<setminus> SCons ?tyid ?dc ?s1'
\<lbrakk>AF_typedef_poly ?tyid ?bva ?dclist \<in> set ?P; atom ?bva \<sharp> (?b1.0, ?bv, ?b', ?s1.0, ?s1'); (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b[?bva::=?b1.0]\<^sub>b\<^sub>b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SConsp ?tyid ?dc ?b1.0[?bv::=?b']\<^sub>b\<^sub>b ?s1.0 ~ B_app ?tyid ?b1.0 [ ?bv ::= ?b' ] \<setminus> SConsp ?tyid ?dc ?b1.0 ?s1'
 ?P  \<turnstile> ?s : B_bitvec \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SBool x ~ b [ bv ::= b' ] \<setminus> a

goal (5 subgoals):
 1. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 2. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 3. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 4. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 2. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 3. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 4. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
case (SPair s1 s2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> T  \<turnstile> s1 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> a
\<lbrakk> T  \<turnstile> s2 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s2 ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SPair s1 s2 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (5 subgoals):
 1. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 2. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 3. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 4. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> T  \<turnstile> s1 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> a
\<lbrakk> T  \<turnstile> s2 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s2 ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SPair s1 s2 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
[PROOF STEP]
obtain b1 and b2 where *:"b[bv::=b']\<^sub>b\<^sub>b = B_pair b1 b2 \<and> wfRCV T s1 b1 \<and> wfRCV T s2 b2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> T  \<turnstile> s1 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> a
\<lbrakk> T  \<turnstile> s2 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s2 ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SPair s1 s2 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. (\<And>b1 b2. b[bv::=b']\<^sub>b\<^sub>b = [ b1 , b2 ]\<^sup>b \<and>  T  \<turnstile> s1 : b1 \<and>  T  \<turnstile> s2 : b2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfRCV_elims(12)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> T  \<turnstile> s1 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> a
\<lbrakk> T  \<turnstile> s2 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s2 ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SPair s1 s2 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
\<lbrakk> ?P  \<turnstile> SPair ?s1.0 ?s2.0 : ?b; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?P  \<turnstile> ?s1.0 : b1;  ?P  \<turnstile> ?s2.0 : b2\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. (\<And>b1 b2. b[bv::=b']\<^sub>b\<^sub>b = [ b1 , b2 ]\<^sup>b \<and>  T  \<turnstile> s1 : b1 \<and>  T  \<turnstile> s2 : b2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b[bv::=b']\<^sub>b\<^sub>b = [ b1 , b2 ]\<^sup>b \<and>  T  \<turnstile> s1 : b1 \<and>  T  \<turnstile> s2 : b2

goal (5 subgoals):
 1. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x1a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x1a b bv b'); \<And>b. \<lbrakk> T  \<turnstile> x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x2a b bv b');  T  \<turnstile> SPair x1a x2a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SPair x1a x2a) b bv b')
 2. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 3. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 4. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
proof (cases "b = B_var bv")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "T  \<turnstile> SPair s1 s2 : B_pair b1 b2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b
[PROOF STEP]
using wfRCV.intros *
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv
b[bv::=b']\<^sub>b\<^sub>b = [ b1 , b2 ]\<^sup>b \<and>  T  \<turnstile> s1 : b1 \<and>  T  \<turnstile> s2 : b2

goal (1 subgoal):
 1.  T  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b' = B_pair b1 b2"
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b

goal (1 subgoal):
 1. b' = [ b1 , b2 ]\<^sup>b
[PROOF STEP]
using True SPair subst_bb.simps(1) *
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b
b = B_var bv
\<lbrakk> T  \<turnstile> s1 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> a
\<lbrakk> T  \<turnstile> s2 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s2 ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SPair s1 s2 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
(B_var ?bv2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = (if ?bv1.0 = ?bv2.0 then ?b else B_var ?bv2.0)
b[bv::=b']\<^sub>b\<^sub>b = [ b1 , b2 ]\<^sup>b \<and>  T  \<turnstile> s1 : b1 \<and>  T  \<turnstile> s2 : b2

goal (1 subgoal):
 1. b' = [ b1 , b2 ]\<^sup>b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b' = [ b1 , b2 ]\<^sup>b

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b = B_var bv
 T  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b
b' = [ b1 , b2 ]\<^sup>b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b
b' = [ b1 , b2 ]\<^sup>b

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using boxed_b_BVar1I
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b
b' = [ b1 , b2 ]\<^sup>b
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> B_var bv
[PROOF STEP]
obtain b1' and b2' where "b = B_pair b1' b2' \<and> b1=b1'[bv::=b']\<^sub>b\<^sub>b \<and> b2=b2'[bv::=b']\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. (\<And>b1' b2'. b = [ b1' , b2' ]\<^sup>b \<and> b1 = b1'[bv::=b']\<^sub>b\<^sub>b \<and> b2 = b2'[bv::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subst_bb_inject(5)[OF _ False ] *
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv
\<lbrakk>?b1.0 = b[bv::=?b]\<^sub>b\<^sub>b; ?b1.0 = [ ?b11.0 , ?b12.0 ]\<^sup>b\<rbrakk> \<Longrightarrow> \<exists>b11' b12'. ?b11.0 = b11'[bv::=?b]\<^sub>b\<^sub>b \<and> ?b12.0 = b12'[bv::=?b]\<^sub>b\<^sub>b \<and> b = [ b11' , b12' ]\<^sup>b
b[bv::=b']\<^sub>b\<^sub>b = [ b1 , b2 ]\<^sup>b \<and>  T  \<turnstile> s1 : b1 \<and>  T  \<turnstile> s2 : b2

goal (1 subgoal):
 1. (\<And>b1' b2'. b = [ b1' , b2' ]\<^sup>b \<and> b1 = b1'[bv::=b']\<^sub>b\<^sub>b \<and> b2 = b2'[bv::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b = [ b1' , b2' ]\<^sup>b \<and> b1 = b1'[bv::=b']\<^sub>b\<^sub>b \<and> b2 = b2'[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = [ b1' , b2' ]\<^sup>b \<and> b1 = b1'[bv::=b']\<^sub>b\<^sub>b \<and> b2 = b2'[bv::=b']\<^sub>b\<^sub>b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = [ b1' , b2' ]\<^sup>b \<and> b1 = b1'[bv::=b']\<^sub>b\<^sub>b \<and> b2 = b2'[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using *  SPair boxed_b_BPairI
[PROOF STATE]
proof (prove)
using this:
b = [ b1' , b2' ]\<^sup>b \<and> b1 = b1'[bv::=b']\<^sub>b\<^sub>b \<and> b2 = b2'[bv::=b']\<^sub>b\<^sub>b
b[bv::=b']\<^sub>b\<^sub>b = [ b1 , b2 ]\<^sup>b \<and>  T  \<turnstile> s1 : b1 \<and>  T  \<turnstile> s2 : b2
\<lbrakk> T  \<turnstile> s1 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> a
\<lbrakk> T  \<turnstile> s2 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s2 ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SPair s1 s2 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
\<lbrakk> ?P  \<turnstile> ?s1.0 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> ?s1' ;  ?P  \<turnstile> ?s2.0 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> ?s2' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> SPair ?s1' ?s2'

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SPair s1 s2 ~ b [ bv ::= b' ] \<setminus> a

goal (4 subgoals):
 1. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 2. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 3. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 2. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 3. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
case (SCons tyid dc s1)
[PROOF STATE]
proof (state)
this:
\<lbrakk> T  \<turnstile> s1 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SCons tyid dc s1 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (4 subgoals):
 1. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 2. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 3. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
have *:"b[bv::=b']\<^sub>b\<^sub>b = B_id tyid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = B_id tyid
[PROOF STEP]
using wfRCV_elims(13)[OF SCons(2)]
[PROOF STATE]
proof (prove)
using this:
(\<And>dclist x b c. \<lbrakk>b[bv::=b']\<^sub>b\<^sub>b = B_id tyid; AF_typedef tyid dclist \<in> set T; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  T  \<turnstile> s1 : b\<rbrakk> \<Longrightarrow> ?Pa) \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = B_id tyid
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b[bv::=b']\<^sub>b\<^sub>b = B_id tyid

goal (4 subgoals):
 1. \<And>x1a x2a x3a b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x3a b bv b');  T  \<turnstile> SCons x1a x2a x3a : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SCons x1a x2a x3a) b bv b')
 2. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 3. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
proof (cases "b = B_var bv")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "T  \<turnstile> SCons tyid dc s1 : B_id tyid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> SCons tyid dc s1 : B_id tyid
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1.  T  \<turnstile> SCons tyid dc s1 : B_id tyid
[PROOF STEP]
using "local.*" SCons.prems
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv
b[bv::=b']\<^sub>b\<^sub>b = B_id tyid
 T  \<turnstile> SCons tyid dc s1 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1.  T  \<turnstile> SCons tyid dc s1 : B_id tyid
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SCons tyid dc s1 : B_id tyid

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SCons tyid dc s1 : B_id tyid

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b' =  B_id tyid"
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SCons tyid dc s1 : B_id tyid

goal (1 subgoal):
 1. b' = B_id tyid
[PROOF STEP]
using True SCons subst_bb.simps(1) *
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SCons tyid dc s1 : B_id tyid
b = B_var bv
\<lbrakk> T  \<turnstile> s1 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SCons tyid dc s1 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
(B_var ?bv2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = (if ?bv1.0 = ?bv2.0 then ?b else B_var ?bv2.0)
b[bv::=b']\<^sub>b\<^sub>b = B_id tyid

goal (1 subgoal):
 1. b' = B_id tyid
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b' = B_id tyid

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b = B_var bv
 T  \<turnstile> SCons tyid dc s1 : B_id tyid
b' = B_id tyid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SCons tyid dc s1 : B_id tyid
b' = B_id tyid

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using boxed_b_BVar1I  wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SCons tyid dc s1 : B_id tyid
b' = B_id tyid
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> B_var bv
[PROOF STEP]
obtain b1' where beq: "b = B_id tyid"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. (b = B_id tyid \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subst_bb_inject *
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_int\<rbrakk> \<Longrightarrow> ?b2.0 = B_int
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_bool\<rbrakk> \<Longrightarrow> ?b2.0 = B_bool
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_unit\<rbrakk> \<Longrightarrow> ?b2.0 = B_unit
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_bitvec\<rbrakk> \<Longrightarrow> ?b2.0 = B_bitvec
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = [ ?b11.0 , ?b12.0 ]\<^sup>b\<rbrakk> \<Longrightarrow> \<exists>b11' b12'. ?b11.0 = b11'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b12.0 = b12'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b2.0 = [ b11' , b12' ]\<^sup>b
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_var ?bv'\<rbrakk> \<Longrightarrow> ?b2.0 = B_var ?bv'
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_id ?tyid\<rbrakk> \<Longrightarrow> ?b2.0 = B_id ?tyid
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_app ?tyid ?b11.0\<rbrakk> \<Longrightarrow> \<exists>b11'. ?b11.0 = b11'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b2.0 = B_app ?tyid b11'
b[bv::=b']\<^sub>b\<^sub>b = B_id tyid

goal (1 subgoal):
 1. (b = B_id tyid \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b = B_id tyid

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = B_id tyid
[PROOF STEP]
obtain b2 dclist x c where **:"AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and> wfRCV T s1 b2"
[PROOF STATE]
proof (prove)
using this:
b = B_id tyid

goal (1 subgoal):
 1. (\<And>dclist x b2 c. AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s1 : b2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfRCV_elims(13)  * SCons
[PROOF STATE]
proof (prove)
using this:
b = B_id tyid
\<lbrakk> ?P  \<turnstile> SCons ?s ?dc ?s1.0 : ?b; \<And>dclist x b c. \<lbrakk>?b = B_id ?s; AF_typedef ?s dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> ?s1.0 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
b[bv::=b']\<^sub>b\<^sub>b = B_id tyid
\<lbrakk> T  \<turnstile> s1 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SCons tyid dc s1 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. (\<And>dclist x b2 c. AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s1 : b2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s1 : b2

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s1 : b2
[PROOF STEP]
have "atom bv \<sharp> b2"
[PROOF STATE]
proof (prove)
using this:
AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s1 : b2

goal (1 subgoal):
 1. atom bv \<sharp> b2
[PROOF STEP]
using \<open>wfTh T\<close> wfTh_lookup_supp_empty[of tyid dclist T dc "\<lbrace> x : b2  | c \<rbrace>"] \<tau>.fresh fresh_def
[PROOF STATE]
proof (prove)
using this:
AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s1 : b2
   \<turnstile>\<^sub>w\<^sub>f T
\<lbrakk>AF_typedef tyid dclist \<in> set T; (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> supp \<lbrace> x : b2  | c \<rbrace> = {}
?a \<sharp> \<lbrace> ?x : ?b  | ?c \<rbrace> = ((?a \<sharp> ?c \<or> ?a \<in> set [atom ?x]) \<and> ?a \<sharp> ?b)
?a \<sharp> ?x \<equiv> ?a \<notin> supp ?x

goal (1 subgoal):
 1. atom bv \<sharp> b2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom bv \<sharp> b2

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom bv \<sharp> b2
[PROOF STEP]
have "b2 = b2[ bv ::= b']\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
atom bv \<sharp> b2

goal (1 subgoal):
 1. b2 = b2[bv::=b']\<^sub>b\<^sub>b
[PROOF STEP]
using forget_subst subst_b_b_def
[PROOF STATE]
proof (prove)
using this:
atom bv \<sharp> b2
atom ?a \<sharp> ?tm \<Longrightarrow> ?tm[?a::=?x]\<^sub>b = ?tm
subst_b = subst_bb_abbrev

goal (1 subgoal):
 1. b2 = b2[bv::=b']\<^sub>b\<^sub>b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b2 = b2[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b2 = b2[bv::=b']\<^sub>b\<^sub>b
[PROOF STEP]
obtain s1' where s1:"T  \<turnstile> s1 ~ b2 [ bv ::= b' ] \<setminus> s1'"
[PROOF STATE]
proof (prove)
using this:
b2 = b2[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. (\<And>s1'.  T  \<turnstile> s1 ~ b2 [ bv ::= b' ] \<setminus> s1'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using SCons **
[PROOF STATE]
proof (prove)
using this:
b2 = b2[bv::=b']\<^sub>b\<^sub>b
\<lbrakk> T  \<turnstile> s1 : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SCons tyid dc s1 : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s1 : b2

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

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "T  \<turnstile> SCons tyid dc s1 ~ (B_id tyid) [ bv ::= b' ] \<setminus> SCons tyid dc s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> SCons tyid dc s1 ~ B_id tyid [ bv ::= b' ] \<setminus> SCons tyid dc s1'
[PROOF STEP]
proof(rule boxed_b_BConsI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. AF_typedef tyid ?dclist \<in> set T
 2. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist
 3.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> s1'
[PROOF STEP]
show "AF_typedef tyid dclist \<in> set T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AF_typedef tyid dclist \<in> set T
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s1 : b2

goal (1 subgoal):
 1. AF_typedef tyid dclist \<in> set T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AF_typedef tyid dclist \<in> set T

goal (2 subgoals):
 1. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set dclist
 2.  T  \<turnstile> s1 ~ ?b [ bv ::= b' ] \<setminus> s1'
[PROOF STEP]
show "(dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s1 : b2

goal (1 subgoal):
 1. (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist

goal (1 subgoal):
 1.  T  \<turnstile> s1 ~ b2 [ bv ::= b' ] \<setminus> s1'
[PROOF STEP]
show "T  \<turnstile> s1 ~ b2 [ bv ::= b' ] \<setminus> s1' "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> s1 ~ b2 [ bv ::= b' ] \<setminus> s1'
[PROOF STEP]
using s1 **
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> s1 ~ b2 [ bv ::= b' ] \<setminus> s1'
AF_typedef tyid dclist \<in> set T \<and> (dc, \<lbrace> x : b2  | c \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s1 : b2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SCons tyid dc s1 ~ B_id tyid [ bv ::= b' ] \<setminus> SCons tyid dc s1'

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SCons tyid dc s1 ~ B_id tyid [ bv ::= b' ] \<setminus> SCons tyid dc s1'

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using beq
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SCons tyid dc s1 ~ B_id tyid [ bv ::= b' ] \<setminus> SCons tyid dc s1'
b = B_id tyid

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SCons tyid dc s1 ~ b [ bv ::= b' ] \<setminus> a

goal (3 subgoals):
 1. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 2. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 2. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
case (SConsp typid dc bdc s)
[PROOF STATE]
proof (state)
this:
\<lbrakk> T  \<turnstile> s : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SConsp typid dc bdc s : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (3 subgoals):
 1. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 2. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
obtain bva dclist x1 b1 c1 where **:"b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and>
    AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bva dclist x1 b1 c1. b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfRCV_poly_elims[OF SConsp(2)]
[PROOF STATE]
proof (prove)
using this:
(\<And>bva dclist x1 b1 c1. b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> ?tm \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>bva dclist x1 b1 c1. b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv

goal (3 subgoals):
 1. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 2. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv
[PROOF STEP]
have *:"B_app typid bdc = b[bv::=b']\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv

goal (1 subgoal):
 1. B_app typid bdc = b[bv::=b']\<^sub>b\<^sub>b
[PROOF STEP]
using wfRCV_elims(14)[OF SConsp(2)]
[PROOF STATE]
proof (prove)
using this:
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv
(\<And>bva dclist x b c. \<lbrakk>b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc; AF_typedef_poly typid bva dclist \<in> set T; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bva \<sharp> (T, SConsp typid dc bdc s, B_app typid bdc);  T  \<turnstile> s : b[bva::=bdc]\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa) \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. B_app typid bdc = b[bv::=b']\<^sub>b\<^sub>b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
B_app typid bdc = b[bv::=b']\<^sub>b\<^sub>b

goal (3 subgoals):
 1. \<And>x1a x2a x3a x4 b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x4 b bv b');  T  \<turnstile> SConsp x1a x2a x3a x4 : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SConsp x1a x2a x3a x4) b bv b')
 2. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
proof (cases "b = B_var bv")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "T  \<turnstile> SConsp typid dc bdc s  : B_app typid bdc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> SConsp typid dc bdc s : B_app typid bdc
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1.  T  \<turnstile> SConsp typid dc bdc s : B_app typid bdc
[PROOF STEP]
using "local.*" SConsp.prems(1)
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv
B_app typid bdc = b[bv::=b']\<^sub>b\<^sub>b
 T  \<turnstile> SConsp typid dc bdc s : b[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1.  T  \<turnstile> SConsp typid dc bdc s : B_app typid bdc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SConsp typid dc bdc s : B_app typid bdc

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SConsp typid dc bdc s : B_app typid bdc

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b' = B_app typid bdc"
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SConsp typid dc bdc s : B_app typid bdc

goal (1 subgoal):
 1. b' = B_app typid bdc
[PROOF STEP]
using True SConsp subst_bb.simps *
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SConsp typid dc bdc s : B_app typid bdc
b = B_var bv
\<lbrakk> T  \<turnstile> s : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SConsp typid dc bdc s : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
(B_var ?bv2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = (if ?bv1.0 = ?bv2.0 then ?b else B_var ?bv2.0)
B_int[?bv1.0::=?b]\<^sub>b\<^sub>b = B_int
B_bool[?bv1.0::=?b]\<^sub>b\<^sub>b = B_bool
(B_id ?s)[?bv1.0::=?b]\<^sub>b\<^sub>b = B_id ?s
[ ?b1.0 , ?b2.0 ]\<^sup>b[?bv1.0::=?b]\<^sub>b\<^sub>b = [ ?b1.0[?bv1.0::=?b]\<^sub>b\<^sub>b , ?b2.0[?bv1.0::=?b]\<^sub>b\<^sub>b ]\<^sup>b
B_unit[?bv1.0::=?b]\<^sub>b\<^sub>b = B_unit
B_bitvec[?bv1.0::=?b]\<^sub>b\<^sub>b = B_bitvec
(B_app ?s ?b2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = B_app ?s ?b2.0[?bv1.0::=?b]\<^sub>b\<^sub>b
B_app typid bdc = b[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. b' = B_app typid bdc
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b' = B_app typid bdc

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b = B_var bv
 T  \<turnstile> SConsp typid dc bdc s : B_app typid bdc
b' = B_app typid bdc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SConsp typid dc bdc s : B_app typid bdc
b' = B_app typid bdc

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using boxed_b.intros  wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SConsp typid dc bdc s : B_app typid bdc
b' = B_app typid bdc
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
\<lbrakk>?bv \<noteq> ?bv';  ?P  \<turnstile> ?s : B_var ?bv'\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_int \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_int [ ?uu ::= ?uv ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_bool \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bool [ ?uw ::= ?ux ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_unit \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_unit [ ?uy ::= ?uz ] \<setminus> ?s
\<lbrakk> ?P  \<turnstile> ?s1.0 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> ?s1' ;  ?P  \<turnstile> ?s2.0 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> ?s2' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> SPair ?s1' ?s2'
\<lbrakk>AF_typedef ?tyid ?dclist \<in> set ?P; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SCons ?tyid ?dc ?s1.0 ~ B_id ?tyid [ ?bv ::= ?b' ] \<setminus> SCons ?tyid ?dc ?s1'
\<lbrakk>AF_typedef_poly ?tyid ?bva ?dclist \<in> set ?P; atom ?bva \<sharp> (?b1.0, ?bv, ?b', ?s1.0, ?s1'); (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b[?bva::=?b1.0]\<^sub>b\<^sub>b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SConsp ?tyid ?dc ?b1.0[?bv::=?b']\<^sub>b\<^sub>b ?s1.0 ~ B_app ?tyid ?b1.0 [ ?bv ::= ?b' ] \<setminus> SConsp ?tyid ?dc ?b1.0 ?s1'
 ?P  \<turnstile> ?s : B_bitvec \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> B_var bv
[PROOF STEP]
obtain bdc' where bdc: "b = B_app typid bdc' \<and> bdc = bdc'[bv::=b']\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. (\<And>bdc'. b = B_app typid bdc' \<and> bdc = bdc'[bv::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using * subst_bb_inject(8)[OF *]
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv
B_app typid bdc = b[bv::=b']\<^sub>b\<^sub>b
\<lbrakk>b \<noteq> B_var bv; B_app typid bdc = B_app ?tyid ?b11.0\<rbrakk> \<Longrightarrow> \<exists>b11'. ?b11.0 = b11'[bv::=b']\<^sub>b\<^sub>b \<and> b = B_app ?tyid b11'

goal (1 subgoal):
 1. (\<And>bdc'. b = B_app typid bdc' \<and> bdc = bdc'[bv::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b = B_app typid bdc' \<and> bdc = bdc'[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
(*hence beq:"b = B_app typid bdc" using subst_bb_inject *  sory (* going to be like the above as bdc is closed *)*)
[PROOF STATE]
proof (state)
this:
b = B_app typid bdc' \<and> bdc = bdc'[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "atom bv \<sharp> b1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom bv \<sharp> b1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atom bv \<sharp> b1
[PROOF STEP]
have "supp b1 \<subseteq> { atom bva }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp b1 \<subseteq> {atom bva}
[PROOF STEP]
using wfTh_poly_supp_b ** SConsp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>AF_typedef_poly ?tid ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?z : ?b  | ?c \<rbrace>) \<in> set ?dclist;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta> \<rbrakk> \<Longrightarrow> supp ?b \<subseteq> {atom ?bv}
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv
\<lbrakk> T  \<turnstile> s : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SConsp typid dc bdc s : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. supp b1 \<subseteq> {atom bva}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
supp b1 \<subseteq> {atom bva}

goal (1 subgoal):
 1. atom bv \<sharp> b1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
supp b1 \<subseteq> {atom bva}

goal (1 subgoal):
 1. atom bv \<sharp> b1
[PROOF STEP]
have "bv \<noteq> bva"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bv \<noteq> bva
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv

goal (1 subgoal):
 1. bv \<noteq> bva
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bv \<noteq> bva

goal (1 subgoal):
 1. atom bv \<sharp> b1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
supp b1 \<subseteq> {atom bva}
bv \<noteq> bva
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
supp b1 \<subseteq> {atom bva}
bv \<noteq> bva

goal (1 subgoal):
 1. atom bv \<sharp> b1
[PROOF STEP]
using fresh_def
[PROOF STATE]
proof (prove)
using this:
supp b1 \<subseteq> {atom bva}
bv \<noteq> bva
?a \<sharp> ?x \<equiv> ?a \<notin> supp ?x

goal (1 subgoal):
 1. atom bv \<sharp> b1
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
atom bv \<sharp> b1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atom bv \<sharp> b1

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv

goal (1 subgoal):
 1.  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "b1[bva::=bdc']\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b = b1[bva::=bdc]\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b1[bva::=bdc']\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b = b1[bva::=bdc]\<^sub>b\<^sub>b
[PROOF STEP]
using bdc subst_bb_commute \<open>atom bv \<sharp> b1\<close>
[PROOF STATE]
proof (prove)
using this:
b = B_app typid bdc' \<and> bdc = bdc'[bv::=b']\<^sub>b\<^sub>b
atom ?j \<sharp> ?A \<Longrightarrow> ?A[?i::=?t]\<^sub>b\<^sub>b[?j::=?u]\<^sub>b\<^sub>b = ?A[?i::=?t[?j::=?u]\<^sub>b\<^sub>b]\<^sub>b\<^sub>b
atom bv \<sharp> b1

goal (1 subgoal):
 1. b1[bva::=bdc']\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b = b1[bva::=bdc]\<^sub>b\<^sub>b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b1[bva::=bdc']\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b = b1[bva::=bdc]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b
b1[bva::=bdc']\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b = b1[bva::=bdc]\<^sub>b\<^sub>b
[PROOF STEP]
obtain s' where s':"T  \<turnstile> s ~ b1[bva::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s'"
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b
b1[bva::=bdc']\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b = b1[bva::=bdc]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. (\<And>s'.  T  \<turnstile> s ~ b1[bva::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using SConsp(1)[of "b1[bva::=bdc']\<^sub>b\<^sub>b"] bdc SConsp
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b
b1[bva::=bdc']\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b = b1[bva::=bdc]\<^sub>b\<^sub>b
\<lbrakk> T  \<turnstile> s : b1[bva::=bdc']\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> s ~ b1[bva::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> a
b = B_app typid bdc' \<and> bdc = bdc'[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>a.  T  \<turnstile> s ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SConsp typid dc bdc s : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

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

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ (B_app typid bdc') [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ B_app typid bdc' [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ B_app typid bdc' [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'
[PROOF STEP]
obtain bva3 and dclist3 where 3:"AF_typedef_poly typid bva3 dclist3 =  AF_typedef_poly typid bva dclist \<and>
            atom bva3 \<sharp> (bdc', bv, b', s, s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bva3 dclist3. AF_typedef_poly typid bva3 dclist3 = AF_typedef_poly typid bva dclist \<and> atom bva3 \<sharp> (bdc', bv, b', s, s') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_fresh_bv
[PROOF STATE]
proof (prove)
using this:
(\<And>bva2 dclist2. AF_typedef_poly ?tyid ?bva ?dclist = AF_typedef_poly ?tyid bva2 dclist2 \<and> atom bva2 \<sharp> ?tm \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>bva3 dclist3. AF_typedef_poly typid bva3 dclist3 = AF_typedef_poly typid bva dclist \<and> atom bva3 \<sharp> (bdc', bv, b', s, s') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
AF_typedef_poly typid bva3 dclist3 = AF_typedef_poly typid bva dclist \<and> atom bva3 \<sharp> (bdc', bv, b', s, s')

goal (1 subgoal):
 1.  T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ B_app typid bdc' [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AF_typedef_poly typid bva3 dclist3 = AF_typedef_poly typid bva dclist \<and> atom bva3 \<sharp> (bdc', bv, b', s, s')
[PROOF STEP]
obtain x3 b3 c3 where 4:"(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3"
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly typid bva3 dclist3 = AF_typedef_poly typid bva dclist \<and> atom bva3 \<sharp> (bdc', bv, b', s, s')

goal (1 subgoal):
 1. (\<And>x3 b3 c3. (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using boxed_b_BConspI td_lookup_eq_iff type_def.eq_iff
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly typid bva3 dclist3 = AF_typedef_poly typid bva dclist \<and> atom bva3 \<sharp> (bdc', bv, b', s, s')
\<lbrakk>AF_typedef_poly ?tyid ?bva ?dclist \<in> set ?P; atom ?bva \<sharp> (?b1.0, ?bv, ?b', ?s1.0, ?s1'); (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b[?bva::=?b1.0]\<^sub>b\<^sub>b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SConsp ?tyid ?dc ?b1.0[?bv::=?b']\<^sub>b\<^sub>b ?s1.0 ~ B_app ?tyid ?b1.0 [ ?bv ::= ?b' ] \<setminus> SConsp ?tyid ?dc ?b1.0 ?s1'
\<lbrakk>[[atom ?bva1.0]]lst. ?dclist1.0 = [[atom ?bva2.0]]lst. ?dclist2.0; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist1.0\<rbrakk> \<Longrightarrow> \<exists>x2 b2 c2. (?dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set ?dclist2.0
(AF_typedef ?list1.0 ?list2.0 = AF_typedef ?list1a ?list2a) = (?list1.0 = ?list1a \<and> ?list2.0 = ?list2a)
(AF_typedef_poly ?list1.0 ?bv ?list2.0 = AF_typedef_poly ?list1a ?bva ?list2a) = ([[atom ?bv]]lst. ?list2.0 = [[atom ?bva]]lst. ?list2a \<and> ?list1.0 = ?list1a)

goal (1 subgoal):
 1. (\<And>x3 b3 c3. (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis "**")
[PROOF STATE]
proof (state)
this:
(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3

goal (1 subgoal):
 1.  T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ B_app typid bdc' [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ B_app typid bdc' [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. AF_typedef_poly typid ?bva ?dclist \<in> set T
 2. atom ?bva \<sharp> (bdc', bv, b', s, s')
 3. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist
 4.  T  \<turnstile> s ~ ?b[?bva::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
show \<open>AF_typedef_poly typid bva3 dclist3 \<in> set T\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AF_typedef_poly typid bva3 dclist3 \<in> set T
[PROOF STEP]
using 3 **
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly typid bva3 dclist3 = AF_typedef_poly typid bva dclist \<and> atom bva3 \<sharp> (bdc', bv, b', s, s')
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv

goal (1 subgoal):
 1. AF_typedef_poly typid bva3 dclist3 \<in> set T
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
AF_typedef_poly typid bva3 dclist3 \<in> set T

goal (3 subgoals):
 1. atom bva3 \<sharp> (bdc', bv, b', s, s')
 2. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set dclist3
 3.  T  \<turnstile> s ~ ?b[bva3::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
show \<open>atom bva3 \<sharp> (bdc', bv, b', s, s')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom bva3 \<sharp> (bdc', bv, b', s, s')
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly typid bva3 dclist3 = AF_typedef_poly typid bva dclist \<and> atom bva3 \<sharp> (bdc', bv, b', s, s')

goal (1 subgoal):
 1. atom bva3 \<sharp> (bdc', bv, b', s, s')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
atom bva3 \<sharp> (bdc', bv, b', s, s')

goal (2 subgoals):
 1. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set dclist3
 2.  T  \<turnstile> s ~ ?b[bva3::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
show 4:\<open>(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3

goal (1 subgoal):
 1. (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3

goal (1 subgoal):
 1.  T  \<turnstile> s ~ b3[bva3::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
have "b3[bva3::=bdc']\<^sub>b\<^sub>b = b1[bva::=bdc']\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b3[bva3::=bdc']\<^sub>b\<^sub>b = b1[bva::=bdc']\<^sub>b\<^sub>b
[PROOF STEP]
proof(rule wfTh_typedef_poly_b_eq_iff)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. AF_typedef_poly ?tyid bva3 ?dclist1.0 \<in> set ?P
 2. (?dc, \<lbrace> ?x1.0 : b3  | ?c1.0 \<rbrace>) \<in> set ?dclist1.0
 3. AF_typedef_poly ?tyid bva ?dclist2.0 \<in> set ?P
 4. (?dc, \<lbrace> ?x2.0 : b1  | ?c2.0 \<rbrace>) \<in> set ?dclist2.0
 5.    \<turnstile>\<^sub>w\<^sub>f ?P
[PROOF STEP]
show \<open>AF_typedef_poly typid bva3 dclist3 \<in> set T\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AF_typedef_poly typid bva3 dclist3 \<in> set T
[PROOF STEP]
using 3 **
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly typid bva3 dclist3 = AF_typedef_poly typid bva dclist \<and> atom bva3 \<sharp> (bdc', bv, b', s, s')
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv

goal (1 subgoal):
 1. AF_typedef_poly typid bva3 dclist3 \<in> set T
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
AF_typedef_poly typid bva3 dclist3 \<in> set T

goal (4 subgoals):
 1. (?dc, \<lbrace> ?x1.0 : b3  | ?c1.0 \<rbrace>) \<in> set dclist3
 2. AF_typedef_poly typid bva ?dclist2.0 \<in> set T
 3. (?dc, \<lbrace> ?x2.0 : b1  | ?c2.0 \<rbrace>) \<in> set ?dclist2.0
 4.    \<turnstile>\<^sub>w\<^sub>f T
[PROOF STEP]
show \<open>(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3

goal (1 subgoal):
 1. (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3

goal (3 subgoals):
 1. AF_typedef_poly typid bva ?dclist2.0 \<in> set T
 2. (dc, \<lbrace> ?x2.0 : b1  | ?c2.0 \<rbrace>) \<in> set ?dclist2.0
 3.    \<turnstile>\<^sub>w\<^sub>f T
[PROOF STEP]
show \<open>AF_typedef_poly typid bva dclist \<in> set T\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AF_typedef_poly typid bva dclist \<in> set T
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv

goal (1 subgoal):
 1. AF_typedef_poly typid bva dclist \<in> set T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AF_typedef_poly typid bva dclist \<in> set T

goal (2 subgoals):
 1. (dc, \<lbrace> ?x2.0 : b1  | ?c2.0 \<rbrace>) \<in> set dclist
 2.    \<turnstile>\<^sub>w\<^sub>f T
[PROOF STEP]
show \<open>(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
b[bv::=b']\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> bv

goal (1 subgoal):
 1. (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist

goal (1 subgoal):
 1.    \<turnstile>\<^sub>w\<^sub>f T
[PROOF STEP]
qed(simp add: ** SConsp)
[PROOF STATE]
proof (state)
this:
b3[bva3::=bdc']\<^sub>b\<^sub>b = b1[bva::=bdc']\<^sub>b\<^sub>b

goal (1 subgoal):
 1.  T  \<turnstile> s ~ b3[bva3::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
thus  \<open> T  \<turnstile> s ~ b3[bva3::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s' \<close>
[PROOF STATE]
proof (prove)
using this:
b3[bva3::=bdc']\<^sub>b\<^sub>b = b1[bva::=bdc']\<^sub>b\<^sub>b

goal (1 subgoal):
 1.  T  \<turnstile> s ~ b3[bva3::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using s'
[PROOF STATE]
proof (prove)
using this:
b3[bva3::=bdc']\<^sub>b\<^sub>b = b1[bva::=bdc']\<^sub>b\<^sub>b
 T  \<turnstile> s ~ b1[bva::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ B_app typid bdc' [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ B_app typid bdc' [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ B_app typid bdc' [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ B_app typid bdc' [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using bdc
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SConsp typid dc bdc'[bv::=b']\<^sub>b\<^sub>b s ~ B_app typid bdc' [ bv ::= b' ] \<setminus> SConsp typid dc bdc' s'
b = B_app typid bdc' \<and> bdc = bdc'[bv::=b']\<^sub>b\<^sub>b

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SConsp typid dc bdc s ~ b [ bv ::= b' ] \<setminus> a

goal (2 subgoals):
 1. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
case SUnit
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (2 subgoals):
 1. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
have *:"b[bv::=b']\<^sub>b\<^sub>b = B_unit"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = B_unit
[PROOF STEP]
using wfRCV_elims SUnit
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?P  \<turnstile> ?s : B_bitvec; \<And>bv. ?s = SBitvec bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : [ ?b1.0 , ?b2.0 ]\<^sup>b; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2;  ?P  \<turnstile> s1 : ?b1.0;  ?P  \<turnstile> s2 : ?b2.0\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_int; \<And>n. ?s = SNum n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_bool; \<And>b. ?s = SBool b \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_id ?ss; \<And>dclist dc x b c s1. \<lbrakk>?s = SCons ?ss dc s1; AF_typedef ?ss dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_var ?bv; \<And>n. ?s = SUt n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_unit; ?s = SUnit \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_app ?tyid ?b; \<And>bv dclist dc x b c s1. \<lbrakk>?s = SConsp ?tyid dc ?b s1; AF_typedef_poly ?tyid bv dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (?P, SConsp ?tyid dc ?b s1, B_app ?tyid ?b);  ?P  \<turnstile> s1 : b[bv::=?b]\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SBitvec ?bv : ?b; ?b = B_bitvec \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SNum ?n : ?b; ?b = B_int \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SBool ?n : ?b; ?b = B_bool \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SPair ?s1.0 ?s2.0 : ?b; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?P  \<turnstile> ?s1.0 : b1;  ?P  \<turnstile> ?s2.0 : b2\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SCons ?s ?dc ?s1.0 : ?b; \<And>dclist x b c. \<lbrakk>?b = B_id ?s; AF_typedef ?s dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> ?s1.0 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : ?b; \<And>bv dclist x b c. \<lbrakk>?b = B_app ?s ?b'; AF_typedef_poly ?s bv dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (?P, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?P  \<turnstile> ?s1.0 : b[bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SUnit : ?b; ?b = B_unit \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SUt ?s1.0 : ?b; \<And>bv. ?b = B_var bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
 T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = B_unit
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b[bv::=b']\<^sub>b\<^sub>b = B_unit

goal (2 subgoals):
 1. \<And>b. \<lbrakk> T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T SUnit b bv b')
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
proof (cases "b = B_var bv")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
have "T  \<turnstile> SUnit : B_unit"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  T  \<turnstile> SUnit : B_unit
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1.  T  \<turnstile> SUnit : B_unit
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SUnit : B_unit

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> SUnit : B_unit

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b' = B_unit"
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SUnit : B_unit

goal (1 subgoal):
 1. b' = B_unit
[PROOF STEP]
using True SUnit subst_bb.simps *
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SUnit : B_unit
b = B_var bv
 T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
(B_var ?bv2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = (if ?bv1.0 = ?bv2.0 then ?b else B_var ?bv2.0)
B_int[?bv1.0::=?b]\<^sub>b\<^sub>b = B_int
B_bool[?bv1.0::=?b]\<^sub>b\<^sub>b = B_bool
(B_id ?s)[?bv1.0::=?b]\<^sub>b\<^sub>b = B_id ?s
[ ?b1.0 , ?b2.0 ]\<^sup>b[?bv1.0::=?b]\<^sub>b\<^sub>b = [ ?b1.0[?bv1.0::=?b]\<^sub>b\<^sub>b , ?b2.0[?bv1.0::=?b]\<^sub>b\<^sub>b ]\<^sup>b
B_unit[?bv1.0::=?b]\<^sub>b\<^sub>b = B_unit
B_bitvec[?bv1.0::=?b]\<^sub>b\<^sub>b = B_bitvec
(B_app ?s ?b2.0)[?bv1.0::=?b]\<^sub>b\<^sub>b = B_app ?s ?b2.0[?bv1.0::=?b]\<^sub>b\<^sub>b
b[bv::=b']\<^sub>b\<^sub>b = B_unit

goal (1 subgoal):
 1. b' = B_unit
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b' = B_unit

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b = B_var bv
 T  \<turnstile> SUnit : B_unit
b' = B_unit
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SUnit : B_unit
b' = B_unit

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using boxed_b.intros  wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
 T  \<turnstile> SUnit : B_unit
b' = B_unit
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
\<lbrakk>?bv \<noteq> ?bv';  ?P  \<turnstile> ?s : B_var ?bv'\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_int \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_int [ ?uu ::= ?uv ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_bool \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bool [ ?uw ::= ?ux ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_unit \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_unit [ ?uy ::= ?uz ] \<setminus> ?s
\<lbrakk> ?P  \<turnstile> ?s1.0 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> ?s1' ;  ?P  \<turnstile> ?s2.0 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> ?s2' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> SPair ?s1' ?s2'
\<lbrakk>AF_typedef ?tyid ?dclist \<in> set ?P; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SCons ?tyid ?dc ?s1.0 ~ B_id ?tyid [ ?bv ::= ?b' ] \<setminus> SCons ?tyid ?dc ?s1'
\<lbrakk>AF_typedef_poly ?tyid ?bva ?dclist \<in> set ?P; atom ?bva \<sharp> (?b1.0, ?bv, ?b', ?s1.0, ?s1'); (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b[?bva::=?b1.0]\<^sub>b\<^sub>b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SConsp ?tyid ?dc ?b1.0[?bv::=?b']\<^sub>b\<^sub>b ?s1.0 ~ B_app ?tyid ?b1.0 [ ?bv ::= ?b' ] \<setminus> SConsp ?tyid ?dc ?b1.0 ?s1'
 ?P  \<turnstile> ?s : B_bitvec \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

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

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
hence "b = B_unit"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b = B_unit
[PROOF STEP]
using subst_bb_inject *
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_int\<rbrakk> \<Longrightarrow> ?b2.0 = B_int
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_bool\<rbrakk> \<Longrightarrow> ?b2.0 = B_bool
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_unit\<rbrakk> \<Longrightarrow> ?b2.0 = B_unit
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_bitvec\<rbrakk> \<Longrightarrow> ?b2.0 = B_bitvec
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = [ ?b11.0 , ?b12.0 ]\<^sup>b\<rbrakk> \<Longrightarrow> \<exists>b11' b12'. ?b11.0 = b11'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b12.0 = b12'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b2.0 = [ b11' , b12' ]\<^sup>b
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_var ?bv'\<rbrakk> \<Longrightarrow> ?b2.0 = B_var ?bv'
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_id ?tyid\<rbrakk> \<Longrightarrow> ?b2.0 = B_id ?tyid
\<lbrakk>?b1.0 = ?b2.0[?bv::=?b]\<^sub>b\<^sub>b; ?b2.0 \<noteq> B_var ?bv; ?b1.0 = B_app ?tyid ?b11.0\<rbrakk> \<Longrightarrow> \<exists>b11'. ?b11.0 = b11'[?bv::=?b]\<^sub>b\<^sub>b \<and> ?b2.0 = B_app ?tyid b11'
b[bv::=b']\<^sub>b\<^sub>b = B_unit

goal (1 subgoal):
 1. b = B_unit
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b = B_unit

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = B_unit
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_unit

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using * SUnit boxed_b.intros
[PROOF STATE]
proof (prove)
using this:
b = B_unit
b[bv::=b']\<^sub>b\<^sub>b = B_unit
 T  \<turnstile> SUnit : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
\<lbrakk>?bv \<noteq> ?bv';  ?P  \<turnstile> ?s : B_var ?bv'\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_int \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_int [ ?uu ::= ?uv ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_bool \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bool [ ?uw ::= ?ux ] \<setminus> ?s
 ?P  \<turnstile> ?s : B_unit \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_unit [ ?uy ::= ?uz ] \<setminus> ?s
\<lbrakk> ?P  \<turnstile> ?s1.0 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> ?s1' ;  ?P  \<turnstile> ?s2.0 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> ?s2' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> SPair ?s1' ?s2'
\<lbrakk>AF_typedef ?tyid ?dclist \<in> set ?P; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SCons ?tyid ?dc ?s1.0 ~ B_id ?tyid [ ?bv ::= ?b' ] \<setminus> SCons ?tyid ?dc ?s1'
\<lbrakk>AF_typedef_poly ?tyid ?bva ?dclist \<in> set ?P; atom ?bva \<sharp> (?b1.0, ?bv, ?b', ?s1.0, ?s1'); (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?P  \<turnstile> ?s1.0 ~ ?b[?bva::=?b1.0]\<^sub>b\<^sub>b [ ?bv ::= ?b' ] \<setminus> ?s1' \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SConsp ?tyid ?dc ?b1.0[?bv::=?b']\<^sub>b\<^sub>b ?s1.0 ~ B_app ?tyid ?b1.0 [ ?bv ::= ?b' ] \<setminus> SConsp ?tyid ?dc ?b1.0 ?s1'
 ?P  \<turnstile> ?s : B_bitvec \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SUnit ~ b [ bv ::= b' ] \<setminus> a

goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
case (SUt x)
[PROOF STATE]
proof (state)
this:
\<lbrakk> T  \<turnstile> x : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> x ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> T  \<turnstile> x : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> x ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
[PROOF STEP]
obtain bv' where *:"b[bv::=b']\<^sub>b\<^sub>b= B_var bv'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> T  \<turnstile> x : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> x ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T

goal (1 subgoal):
 1. (\<And>bv'. b[bv::=b']\<^sub>b\<^sub>b = B_var bv' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfRCV_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> T  \<turnstile> x : ?b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> \<exists>a.  T  \<turnstile> x ~ ?b [ bv ::= b' ] \<setminus> a
 T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f T
\<lbrakk> ?P  \<turnstile> ?s : B_bitvec; \<And>bv. ?s = SBitvec bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : [ ?b1.0 , ?b2.0 ]\<^sup>b; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2;  ?P  \<turnstile> s1 : ?b1.0;  ?P  \<turnstile> s2 : ?b2.0\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_int; \<And>n. ?s = SNum n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_bool; \<And>b. ?s = SBool b \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_id ?ss; \<And>dclist dc x b c s1. \<lbrakk>?s = SCons ?ss dc s1; AF_typedef ?ss dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_var ?bv; \<And>n. ?s = SUt n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_unit; ?s = SUnit \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_app ?tyid ?b; \<And>bv dclist dc x b c s1. \<lbrakk>?s = SConsp ?tyid dc ?b s1; AF_typedef_poly ?tyid bv dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (?P, SConsp ?tyid dc ?b s1, B_app ?tyid ?b);  ?P  \<turnstile> s1 : b[bv::=?b]\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SBitvec ?bv : ?b; ?b = B_bitvec \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SNum ?n : ?b; ?b = B_int \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SBool ?n : ?b; ?b = B_bool \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SPair ?s1.0 ?s2.0 : ?b; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?P  \<turnstile> ?s1.0 : b1;  ?P  \<turnstile> ?s2.0 : b2\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SCons ?s ?dc ?s1.0 : ?b; \<And>dclist x b c. \<lbrakk>?b = B_id ?s; AF_typedef ?s dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> ?s1.0 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : ?b; \<And>bv dclist x b c. \<lbrakk>?b = B_app ?s ?b'; AF_typedef_poly ?s bv dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (?P, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?P  \<turnstile> ?s1.0 : b[bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SUnit : ?b; ?b = B_unit \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SUt ?s1.0 : ?b; \<And>bv. ?b = B_var bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. (\<And>bv'. b[bv::=b']\<^sub>b\<^sub>b = B_var bv' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b[bv::=b']\<^sub>b\<^sub>b = B_var bv'

goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> T  \<turnstile> x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T x b bv b');  T  \<turnstile> SUt x : b[bv::=b']\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f T \<rbrakk> \<Longrightarrow> Ex (boxed_b T (SUt x) b bv b')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
proof (cases "b = B_var bv")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = B_var bv

goal (2 subgoals):
 1. b = B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
 2. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = B_var bv
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = B_var bv

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using boxed_b_BVar1I
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using "local.*" wfRCV_BVarI
[PROOF STATE]
proof (prove)
using this:
b = B_var bv
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
b[bv::=b']\<^sub>b\<^sub>b = B_var bv'
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. b \<noteq> B_var bv \<Longrightarrow> \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> B_var bv
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using boxed_b_BVar1I  boxed_b_BVar2I
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
\<lbrakk>?bv \<noteq> ?bv';  ?P  \<turnstile> ?s : B_var ?bv'\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> ?s

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
using "local.*" wfRCV_BVarI
[PROOF STATE]
proof (prove)
using this:
b \<noteq> B_var bv
\<lbrakk>?bv = ?bv';  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> SUt ?s
\<lbrakk>?bv \<noteq> ?bv';  ?P  \<turnstile> ?s : B_var ?bv'\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s ~ B_var ?bv' [ ?bv ::= ?b ] \<setminus> ?s
b[bv::=b']\<^sub>b\<^sub>b = B_var bv'
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1. \<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a
[PROOF STEP]
by (metis subst_b_var)
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a.  T  \<turnstile> SUt x ~ b [ bv ::= b' ] \<setminus> a

goal:
No subgoals!
[PROOF STEP]
qed