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

goal (1 subgoal):
 1.  P  \<turnstile> s : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s' : b
[PROOF STEP]
proof(induct rule: boxed_b.inducts)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>bv bv' P s b. \<lbrakk>bv = bv';  P  \<turnstile> s : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : (B_var bv')[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SUt s : B_var bv'
 2. \<And>bv bv' P s b. \<lbrakk>bv \<noteq> bv';  P  \<turnstile> s : B_var bv';    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : (B_var bv')[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_var bv'
 3. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 4. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 5. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 6. \<And>P s1 b1 bv b s1' s2 b2 s2'. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1;  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SPair s1' s2' : [ b1 , b2 ]\<^sup>b
 7. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 8. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 9. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
case (boxed_b_BVar1I bv bv' P s b )
[PROOF STATE]
proof (state)
this:
bv = bv'
 P  \<turnstile> s : b
   \<turnstile>\<^sub>w\<^sub>f P

goal (9 subgoals):
 1. \<And>bv bv' P s b. \<lbrakk>bv = bv';  P  \<turnstile> s : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : (B_var bv')[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SUt s : B_var bv'
 2. \<And>bv bv' P s b. \<lbrakk>bv \<noteq> bv';  P  \<turnstile> s : B_var bv';    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : (B_var bv')[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_var bv'
 3. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 4. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 5. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 6. \<And>P s1 b1 bv b s1' s2 b2 s2'. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1;  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SPair s1' s2' : [ b1 , b2 ]\<^sup>b
 7. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 8. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 9. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bv = bv'
 P  \<turnstile> s : b
   \<turnstile>\<^sub>w\<^sub>f P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bv = bv'
 P  \<turnstile> s : b
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1.  P  \<turnstile> s : (B_var bv')[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SUt s : B_var bv'
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
bv = bv'
 P  \<turnstile> s : b
   \<turnstile>\<^sub>w\<^sub>f P
 ?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.  P  \<turnstile> s : (B_var bv')[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SUt s : B_var bv'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s : (B_var bv')[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SUt s : B_var bv'

goal (8 subgoals):
 1. \<And>bv bv' P s b. \<lbrakk>bv \<noteq> bv';  P  \<turnstile> s : B_var bv';    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : (B_var bv')[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_var bv'
 2. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 3. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 4. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 5. \<And>P s1 b1 bv b s1' s2 b2 s2'. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1;  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SPair s1' s2' : [ b1 , b2 ]\<^sup>b
 6. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 7. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 8. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>bv bv' P s b. \<lbrakk>bv \<noteq> bv';  P  \<turnstile> s : B_var bv';    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : (B_var bv')[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_var bv'
 2. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 3. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 4. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 5. \<And>P s1 b1 bv b s1' s2 b2 s2'. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1;  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SPair s1' s2' : [ b1 , b2 ]\<^sup>b
 6. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 7. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 8. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
case (boxed_b_BVar2I bv bv' P s )
[PROOF STATE]
proof (state)
this:
bv \<noteq> bv'
 P  \<turnstile> s : B_var bv'
   \<turnstile>\<^sub>w\<^sub>f P

goal (8 subgoals):
 1. \<And>bv bv' P s b. \<lbrakk>bv \<noteq> bv';  P  \<turnstile> s : B_var bv';    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : (B_var bv')[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_var bv'
 2. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 3. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 4. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 5. \<And>P s1 b1 bv b s1' s2 b2 s2'. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1;  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SPair s1' s2' : [ b1 , b2 ]\<^sup>b
 6. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 7. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 8. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bv \<noteq> bv'
 P  \<turnstile> s : B_var bv'
   \<turnstile>\<^sub>w\<^sub>f P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bv \<noteq> bv'
 P  \<turnstile> s : B_var bv'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1.  P  \<turnstile> s : (B_var bv')[bv::=b_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_var bv'
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
bv \<noteq> bv'
 P  \<turnstile> s : B_var bv'
   \<turnstile>\<^sub>w\<^sub>f P
 ?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.  P  \<turnstile> s : (B_var bv')[bv::=b_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_var bv'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s : (B_var bv')[bv::=b_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_var bv'

goal (7 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>P s1 b1 bv b s1' s2 b2 s2'. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1;  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SPair s1' s2' : [ b1 , b2 ]\<^sup>b
 5. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 6. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 7. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>P s1 b1 bv b s1' s2 b2 s2'. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1;  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SPair s1' s2' : [ b1 , b2 ]\<^sup>b
 5. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 6. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 7. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
case (boxed_b_BPairI P s1 b1 bv b s1' s2 b2 s2')
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1
 P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2
   \<turnstile>\<^sub>w\<^sub>f P

goal (7 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>P s1 b1 bv b s1' s2 b2 s2'. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1;  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SPair s1' s2' : [ b1 , b2 ]\<^sup>b
 5. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 6. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 7. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1
 P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2
   \<turnstile>\<^sub>w\<^sub>f P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1
 P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1.  P  \<turnstile> SPair s1 s2 : [ b1 , b2 ]\<^sup>b[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> SPair s1' s2' : [ b1 , b2 ]\<^sup>b
[PROOF STEP]
using wfRCV.intros rcl_val.supp
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b1[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b1
 P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s2 : b2[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s2' : b2
   \<turnstile>\<^sub>w\<^sub>f P
 ?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
supp (SBitvec ?list) = supp ?list
supp (SNum ?int) = supp ?int
supp (SBool ?bool) = supp ?bool
supp (SPair ?rcl_val1.0 ?rcl_val2.0) = supp ?rcl_val1.0 \<union> supp ?rcl_val2.0
supp (SCons ?list1.0 ?list2.0 ?rcl_val) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?rcl_val)
supp (SConsp ?list1.0 ?list2.0 ?b ?rcl_val) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?rcl_val))
supp SUnit = {}
supp (SUt ?rcl_val) = supp ?rcl_val

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

goal (6 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 6. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 6. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
case (boxed_b_BConsI tyid dclist P dc x b c s1 bv b' s1')
[PROOF STATE]
proof (state)
this:
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b
   \<turnstile>\<^sub>w\<^sub>f P

goal (6 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 6. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
hence "supp b = {}"
[PROOF STATE]
proof (prove)
using this:
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. supp b = {}
[PROOF STEP]
using wfTh_supp_b
[PROOF STATE]
proof (prove)
using this:
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b
   \<turnstile>\<^sub>w\<^sub>f P
\<lbrakk>AF_typedef ?tid ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?z : ?b  | ?c \<rbrace>) \<in> set ?dclist;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta> \<rbrakk> \<Longrightarrow> supp ?b = {}

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

goal (6 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 6. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
hence "b [ bv ::= b' ]\<^sub>b\<^sub>b = b"
[PROOF STATE]
proof (prove)
using this:
supp b = {}

goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = b
[PROOF STEP]
using fresh_def subst_b_b_def forget_subst[of "bv" b b']
[PROOF STATE]
proof (prove)
using this:
supp b = {}
?a \<sharp> ?x \<equiv> ?a \<notin> supp ?x
subst_b = subst_bb_abbrev
atom bv \<sharp> b \<Longrightarrow> b[bv::=b']\<^sub>b = b

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

goal (6 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 6. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
hence " P  \<turnstile> SCons tyid dc s1 : (B_id tyid)"
[PROOF STATE]
proof (prove)
using this:
b[bv::=b']\<^sub>b\<^sub>b = b

goal (1 subgoal):
 1.  P  \<turnstile> SCons tyid dc s1 : B_id tyid
[PROOF STEP]
using  wfRCV.intros rcl_val.supp subst_bb.simps boxed_b_BConsI
[PROOF STATE]
proof (prove)
using this:
b[bv::=b']\<^sub>b\<^sub>b = b
 ?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
supp (SBitvec ?list) = supp ?list
supp (SNum ?int) = supp ?int
supp (SBool ?bool) = supp ?bool
supp (SPair ?rcl_val1.0 ?rcl_val2.0) = supp ?rcl_val1.0 \<union> supp ?rcl_val2.0
supp (SCons ?list1.0 ?list2.0 ?rcl_val) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?rcl_val)
supp (SConsp ?list1.0 ?list2.0 ?b ?rcl_val) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?rcl_val))
supp SUnit = {}
supp (SUt ?rcl_val) = supp ?rcl_val
(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
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b
   \<turnstile>\<^sub>w\<^sub>f P

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

goal (6 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 6. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> SCons tyid dc s1 : B_id tyid

goal (6 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 6. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
have "P  \<turnstile> SCons tyid dc s1' : B_id tyid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> SCons tyid dc s1' : B_id tyid
[PROOF STEP]
using boxed_b_BConsI
[PROOF STATE]
proof (prove)
using this:
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1.  P  \<turnstile> SCons tyid dc s1' : B_id tyid
[PROOF STEP]
using  wfRCV.intros rcl_val.supp subst_bb.simps boxed_b_BConsI
[PROOF STATE]
proof (prove)
using this:
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b
   \<turnstile>\<^sub>w\<^sub>f P
 ?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
supp (SBitvec ?list) = supp ?list
supp (SNum ?int) = supp ?int
supp (SBool ?bool) = supp ?bool
supp (SPair ?rcl_val1.0 ?rcl_val2.0) = supp ?rcl_val1.0 \<union> supp ?rcl_val2.0
supp (SCons ?list1.0 ?list2.0 ?rcl_val) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?rcl_val)
supp (SConsp ?list1.0 ?list2.0 ?b ?rcl_val) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?rcl_val))
supp SUnit = {}
supp (SUt ?rcl_val) = supp ?rcl_val
(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
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b
   \<turnstile>\<^sub>w\<^sub>f P

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

goal (6 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid dclist P dc x b c s1 bv b' s1'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 6. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 P  \<turnstile> SCons tyid dc s1 : B_id tyid
 P  \<turnstile> SCons tyid dc s1' : B_id tyid
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> SCons tyid dc s1 : B_id tyid
 P  \<turnstile> SCons tyid dc s1' : B_id tyid

goal (1 subgoal):
 1.  P  \<turnstile> SCons tyid dc s1 : (B_id tyid)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SCons tyid dc s1' : B_id tyid
[PROOF STEP]
using subst_bb.simps
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> SCons tyid dc s1 : B_id tyid
 P  \<turnstile> SCons tyid dc s1' : B_id tyid
(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

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

goal (5 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 5. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 5. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
case (boxed_b_BConspI tyid bva dclist P b1 bv b' s1 s1' dc x b c)
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P

goal (5 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 5. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
obtain bva2 and dclist2 where *:"AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and>
             atom bva2 \<sharp> (bv,(P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bva2 dclist2. AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and> atom bva2 \<sharp> (bv, P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b) \<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>bva2 dclist2. AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and> atom bva2 \<sharp> (bv, P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and> atom bva2 \<sharp> (bv, P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)

goal (5 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 5. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and> atom bva2 \<sharp> (bv, P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
[PROOF STEP]
obtain x2 and b2 and c2 where **:\<open>(dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2\<close>
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and> atom bva2 \<sharp> (bv, P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)

goal (1 subgoal):
 1. (\<And>x2 b2 c2. (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2 \<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 tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and> atom bva2 \<sharp> (bv, P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P
\<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>x2 b2 c2. (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (5 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 5. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
have  "P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : B_app tyid b1[bv::=b']\<^sub>b\<^sub>b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. AF_typedef_poly tyid ?bv ?dclist \<in> set P
 2. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist
 3. atom ?bv \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
 4.  P  \<turnstile> s1 : ?b[?bv::=b1[bv::=b']\<^sub>b\<^sub>b]\<^sub>b\<^sub>b
[PROOF STEP]
show 1: \<open>AF_typedef_poly tyid bva2 dclist2 \<in> set P\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AF_typedef_poly tyid bva2 dclist2 \<in> set P
[PROOF STEP]
using boxed_b_BConspI *
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P
AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and> atom bva2 \<sharp> (bv, P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)

goal (1 subgoal):
 1. AF_typedef_poly tyid bva2 dclist2 \<in> set P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bva2 dclist2 \<in> set P

goal (3 subgoals):
 1. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set dclist2
 2. atom bva2 \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
 3.  P  \<turnstile> s1 : ?b[bva2::=b1[bv::=b']\<^sub>b\<^sub>b]\<^sub>b\<^sub>b
[PROOF STEP]
show 2: \<open>(dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
[PROOF STEP]
using boxed_b_BConspI
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P
(dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (1 subgoal):
 1. (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (2 subgoals):
 1. atom bva2 \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
 2.  P  \<turnstile> s1 : b2[bva2::=b1[bv::=b']\<^sub>b\<^sub>b]\<^sub>b\<^sub>b
[PROOF STEP]
hence "atom bv \<sharp> b2"
[PROOF STATE]
proof (prove)
using this:
(dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (1 subgoal):
 1. atom bv \<sharp> b2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2 \<Longrightarrow> atom bv \<sharp> b2
[PROOF STEP]
have "supp b2 \<subseteq> { atom bva2 }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp b2 \<subseteq> {atom bva2}
[PROOF STEP]
using wfTh_poly_supp_b 1 2 boxed_b_BConspI
[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}
AF_typedef_poly tyid bva2 dclist2 \<in> set P
(dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P

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

goal (1 subgoal):
 1. (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2 \<Longrightarrow> atom bv \<sharp> b2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
supp b2 \<subseteq> {atom bva2}

goal (1 subgoal):
 1. (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2 \<Longrightarrow> atom bv \<sharp> b2
[PROOF STEP]
have "bv \<noteq> bva2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bv \<noteq> bva2
[PROOF STEP]
using  * fresh_Pair fresh_at_base
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and> atom bva2 \<sharp> (bv, P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
?a \<sharp> (?x, ?y) = (?a \<sharp> ?x \<and> ?a \<sharp> ?y)
sort_of ?a \<noteq> sort_of (atom ?b) \<Longrightarrow> ?a \<sharp> ?b
?a \<sharp> ?b = (?a \<noteq> atom ?b)

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

goal (1 subgoal):
 1. (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2 \<Longrightarrow> atom bv \<sharp> b2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
supp b2 \<subseteq> {atom bva2}
bv \<noteq> bva2
[PROOF STEP]
show  ?thesis
[PROOF STATE]
proof (prove)
using this:
supp b2 \<subseteq> {atom bva2}
bv \<noteq> bva2

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

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

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

goal (2 subgoals):
 1. atom bva2 \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
 2.  P  \<turnstile> s1 : b2[bva2::=b1[bv::=b']\<^sub>b\<^sub>b]\<^sub>b\<^sub>b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom bv \<sharp> b2

goal (2 subgoals):
 1. atom bva2 \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
 2.  P  \<turnstile> s1 : b2[bva2::=b1[bv::=b']\<^sub>b\<^sub>b]\<^sub>b\<^sub>b
[PROOF STEP]
have "b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b
[PROOF STEP]
using wfTh_typedef_poly_b_eq_iff * 2 boxed_b_BConspI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>AF_typedef_poly ?tyid ?bva1.0 ?dclist1.0 \<in> set ?P; (?dc, \<lbrace> ?x1.0 : ?b1.0  | ?c1.0 \<rbrace>) \<in> set ?dclist1.0; AF_typedef_poly ?tyid ?bva2.0 ?dclist2.0 \<in> set ?P; (?dc, \<lbrace> ?x2.0 : ?b2.0  | ?c2.0 \<rbrace>) \<in> set ?dclist2.0;    \<turnstile>\<^sub>w\<^sub>f ?P \<rbrakk> \<Longrightarrow> ?b1.0[?bva1.0::=?b]\<^sub>b\<^sub>b = ?b2.0[?bva2.0::=?b]\<^sub>b\<^sub>b
AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and> atom bva2 \<sharp> (bv, P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
(dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P

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

goal (2 subgoals):
 1. atom bva2 \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
 2.  P  \<turnstile> s1 : b2[bva2::=b1[bv::=b']\<^sub>b\<^sub>b]\<^sub>b\<^sub>b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
atom bv \<sharp> b2
b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b
[PROOF STEP]
show \<open> P  \<turnstile> s1 : b2[bva2::=b1[bv::=b']\<^sub>b\<^sub>b]\<^sub>b\<^sub>b\<close>
[PROOF STATE]
proof (prove)
using this:
atom bv \<sharp> b2
b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b

goal (1 subgoal):
 1.  P  \<turnstile> s1 : b2[bva2::=b1[bv::=b']\<^sub>b\<^sub>b]\<^sub>b\<^sub>b
[PROOF STEP]
using boxed_b_BConspI subst_b_b_def subst_bb_commute
[PROOF STATE]
proof (prove)
using this:
atom bv \<sharp> b2
b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P
subst_b = subst_bb_abbrev
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

goal (1 subgoal):
 1.  P  \<turnstile> s1 : b2[bva2::=b1[bv::=b']\<^sub>b\<^sub>b]\<^sub>b\<^sub>b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s1 : b2[bva2::=b1[bv::=b']\<^sub>b\<^sub>b]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. atom bva2 \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
[PROOF STEP]
show "atom bva2 \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom bva2 \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
[PROOF STEP]
using * fresh_Pair
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 \<and> atom bva2 \<sharp> (bv, P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
?a \<sharp> (?x, ?y) = (?a \<sharp> ?x \<and> ?a \<sharp> ?y)

goal (1 subgoal):
 1. atom bva2 \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
atom bva2 \<sharp> (P, SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1, B_app tyid b1[bv::=b']\<^sub>b\<^sub>b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : B_app tyid b1[bv::=b']\<^sub>b\<^sub>b

goal (5 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 5. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : B_app tyid b1[bv::=b']\<^sub>b\<^sub>b

goal (5 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 5. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
have "P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. AF_typedef_poly tyid ?bv ?dclist \<in> set P
 2. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist
 3. atom ?bv \<sharp> (P, SConsp tyid dc b1 s1', B_app tyid b1)
 4.  P  \<turnstile> s1' : ?b[?bv::=b1]\<^sub>b\<^sub>b
[PROOF STEP]
show \<open>AF_typedef_poly tyid bva dclist \<in> set P\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AF_typedef_poly tyid bva dclist \<in> set P
[PROOF STEP]
using boxed_b_BConspI
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P

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

goal (3 subgoals):
 1. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set dclist
 2. atom bva \<sharp> (P, SConsp tyid dc b1 s1', B_app tyid b1)
 3.  P  \<turnstile> s1' : ?b[bva::=b1]\<^sub>b\<^sub>b
[PROOF STEP]
show \<open>(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
[PROOF STEP]
using boxed_b_BConspI
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P

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

goal (2 subgoals):
 1. atom bva \<sharp> (P, SConsp tyid dc b1 s1', B_app tyid b1)
 2.  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
[PROOF STEP]
show \<open> P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
[PROOF STEP]
using boxed_b_BConspI
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P

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

goal (1 subgoal):
 1. atom bva \<sharp> (P, SConsp tyid dc b1 s1', B_app tyid b1)
[PROOF STEP]
have "atom bva \<sharp> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom bva \<sharp> P
[PROOF STEP]
using boxed_b_BConspI wfTh_fresh
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P
   \<turnstile>\<^sub>w\<^sub>f ?T  \<Longrightarrow> atom ?x \<sharp> ?T

goal (1 subgoal):
 1. atom bva \<sharp> P
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
atom bva \<sharp> P

goal (1 subgoal):
 1. atom bva \<sharp> (P, SConsp tyid dc b1 s1', B_app tyid b1)
[PROOF STEP]
thus  "atom bva \<sharp> (P, SConsp tyid dc b1 s1', B_app tyid b1)"
[PROOF STATE]
proof (prove)
using this:
atom bva \<sharp> P

goal (1 subgoal):
 1. atom bva \<sharp> (P, SConsp tyid dc b1 s1', B_app tyid b1)
[PROOF STEP]
using boxed_b_BConspI rcl_val.fresh b.fresh pure_fresh fresh_prodN
[PROOF STATE]
proof (prove)
using this:
atom bva \<sharp> P
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b
   \<turnstile>\<^sub>w\<^sub>f P
?a \<sharp> SBitvec ?list = ?a \<sharp> ?list
?a \<sharp> SNum ?int = ?a \<sharp> ?int
?a \<sharp> SBool ?bool = ?a \<sharp> ?bool
?a \<sharp> SPair ?rcl_val1.0 ?rcl_val2.0 = (?a \<sharp> ?rcl_val1.0 \<and> ?a \<sharp> ?rcl_val2.0)
?a \<sharp> SCons ?list1.0 ?list2.0 ?rcl_val = (?a \<sharp> ?list1.0 \<and> ?a \<sharp> ?list2.0 \<and> ?a \<sharp> ?rcl_val)
?a \<sharp> SConsp ?list1.0 ?list2.0 ?b ?rcl_val = (?a \<sharp> ?list1.0 \<and> ?a \<sharp> ?list2.0 \<and> ?a \<sharp> ?b \<and> ?a \<sharp> ?rcl_val)
?a \<sharp> SUnit
?a \<sharp> SUt ?rcl_val = ?a \<sharp> ?rcl_val
?a \<sharp> B_int
?a \<sharp> B_bool
?a \<sharp> B_id ?list = ?a \<sharp> ?list
?a \<sharp> [ ?b1.0 , ?b2.0 ]\<^sup>b = (?a \<sharp> ?b1.0 \<and> ?a \<sharp> ?b2.0)
?a \<sharp> B_unit
?a \<sharp> B_bitvec
?a \<sharp> B_var ?bv = ?a \<sharp> ?bv
?a \<sharp> B_app ?list ?b = (?a \<sharp> ?list \<and> ?a \<sharp> ?b)
?a \<sharp> ?x
?a \<sharp> (?x, ?y) = (?a \<sharp> ?x \<and> ?a \<sharp> ?y)
?x \<sharp> (?a, ?b, ?c) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c)
?x \<sharp> (?a, ?b, ?c, ?d) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d)
?x \<sharp> (?a, ?b, ?c, ?d, ?e) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h, ?i) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h \<and> ?x \<sharp> ?i)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h, ?i, ?j) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h \<and> ?x \<sharp> ?i \<and> ?x \<sharp> ?j)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h, ?i, ?j, ?k, ?l) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h \<and> ?x \<sharp> ?i \<and> ?x \<sharp> ?j \<and> ?x \<sharp> ?k \<and> ?x \<sharp> ?l)

goal (1 subgoal):
 1. atom bva \<sharp> (P, SConsp tyid dc b1 s1', B_app tyid b1)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
atom bva \<sharp> (P, SConsp tyid dc b1 s1', B_app tyid b1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1

goal (5 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f P  \<Longrightarrow>  P  \<turnstile> s1 : b[bva::=b1]\<^sub>b\<^sub>b[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> s1' : b[bva::=b1]\<^sub>b\<^sub>b;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
 5. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : B_app tyid b1[bv::=b']\<^sub>b\<^sub>b
 P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : B_app tyid b1[bv::=b']\<^sub>b\<^sub>b
 P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1

goal (1 subgoal):
 1.  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
[PROOF STEP]
using subst_bb.simps
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : B_app tyid b1[bv::=b']\<^sub>b\<^sub>b
 P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
(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

goal (1 subgoal):
 1.  P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 : (B_app tyid b1)[bv::=b']\<^sub>b\<^sub>b \<and>  P  \<turnstile> SConsp tyid dc b1 s1' : B_app tyid b1

goal (4 subgoals):
 1. \<And>P s uu_ uv_. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_int[uu_::=uv_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_int
 2. \<And>P s uw_ ux_. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bool[uw_::=ux_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bool
 3. \<And>P s uy_ uz_. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_unit[uy_::=uz_]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_unit
 4. \<And>P s bv b. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow>  P  \<turnstile> s : B_bitvec[bv::=b]\<^sub>b\<^sub>b \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
qed(auto)+


[STATEMENT]
lemma is_satis_g_bs_boxed:
  fixes G::\<Gamma>
  assumes  "boxed_i \<Theta> G b bv i i'" and "wfI \<Theta> G[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "wfI \<Theta> G i'"  and "wfG \<Theta> B G"
    and "(i \<Turnstile> G[bv::=b]\<^sub>\<Gamma>\<^sub>b) "
  shows  "(i' \<Turnstile> G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<Turnstile> G
[PROOF STEP]
using is_satis_g_bs_boxed_aux assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta>  ; ?G1.0 ; ?b , ?bv \<turnstile> ?i \<approx> ?i';  ?\<Theta> ; ?G1.0[?bv::=?b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;  ?\<Theta> ; ?G1.0 \<turnstile> ?i'; ?G1.0 = ?G2.0 @ ?G;  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?G1.0 ;  ?i \<Turnstile> ?G[?bv::=?b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  ?i' \<Turnstile> ?G
 \<Theta>  ; G ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; G \<turnstile> i'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G
 i \<Turnstile> G[bv::=b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1.  i' \<Turnstile> G
[PROOF STEP]
by (metis (full_types) append_g.simps(1))