[STATEMENT]
lemma boxed_i_eval_v_boxed_b:
  fixes v::v
  assumes "boxed_i \<Theta> \<Gamma> b' bv i i'" and "i \<lbrakk> v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~  s" and  "i' \<lbrakk> v \<rbrakk> ~ s'" and "wfV \<Theta> B \<Gamma> v b"  and "wfI \<Theta>  \<Gamma> i'"
  shows "boxed_b \<Theta> s b bv b' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
proof(nominal_induct v arbitrary: s s' b  rule:v.strong_induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 5. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
case (V_lit l)
[PROOF STATE]
proof (state)
this:
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ l ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ l ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (5 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 5. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
hence "\<lbrakk> l \<rbrakk> = s \<and> \<lbrakk> l \<rbrakk> = s'"
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ l ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ l ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1. \<lbrakk> l \<rbrakk>  = s \<and> \<lbrakk> l \<rbrakk>  = s'
[PROOF STEP]
using eval_v_elims
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ l ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ l ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<lbrakk> l \<rbrakk>  = s \<and> \<lbrakk> l \<rbrakk>  = s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk> l \<rbrakk>  = s \<and> \<lbrakk> l \<rbrakk>  = s'

goal (5 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 5. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk> l \<rbrakk>  = s \<and> \<lbrakk> l \<rbrakk>  = s'

goal (5 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 5. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
have "b = base_for_lit l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = base_for_lit l
[PROOF STEP]
using wfV_elims(2) V_lit
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : ?b ; \<lbrakk>?b = base_for_lit ?l;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ l ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ l ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

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

goal (5 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 5. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> l \<rbrakk>  = s \<and> \<lbrakk> l \<rbrakk>  = s'
b = base_for_lit l
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> l \<rbrakk>  = s \<and> \<lbrakk> l \<rbrakk>  = s'
b = base_for_lit l

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using V_lit
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> l \<rbrakk>  = s \<and> \<lbrakk> l \<rbrakk>  = s'
b = base_for_lit l
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ l ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ l ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using  eval_l_boxed_b subst_b_base_for_lit
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> l \<rbrakk>  = s \<and> \<lbrakk> l \<rbrakk>  = s'
b = base_for_lit l
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ l ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ l ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'
\<lbrakk> ?l \<rbrakk>  = ?s \<Longrightarrow>  ?\<Theta>  \<turnstile> ?s ~ base_for_lit ?l [ ?bv ::= ?b' ] \<setminus> ?s
(base_for_lit ?l)[?bv::=?b]\<^sub>b\<^sub>b = base_for_lit ?l

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

goal (4 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
case (V_var x)
[PROOF STATE]
proof (state)
this:
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (4 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
(* look at defn of bs_boxed *)
[PROOF STATE]
proof (state)
this:
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (4 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
hence "Some s = i x \<and> Some s' = i' x"
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1. Some s = i x \<and> Some s' = i' x
[PROOF STEP]
using eval_v_elims subst_vb.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?y ]\<^sup>v
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>b = V_cons ?tyid ?c (?v'[?x::=?v]\<^sub>v\<^sub>b)
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>b = V_consp ?tyid ?c ?b[?x::=?v]\<^sub>b\<^sub>b (?v'[?x::=?v]\<^sub>v\<^sub>b)
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>b , ?v2.0[?x::=?v]\<^sub>v\<^sub>b ]\<^sup>v

goal (1 subgoal):
 1. Some s = i x \<and> Some s' = i' x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Some s = i x \<and> Some s' = i' x

goal (4 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Some s = i x \<and> Some s' = i' x

goal (4 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
obtain c1  where bc:"Some (b,c1) = lookup \<Gamma> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c1. Some (b, c1) = lookup \<Gamma> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfV_elims V_var
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?x ]\<^sup>v : ?b ; \<And>c. \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; Some (?b, c) = lookup ?\<Gamma> ?x\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : ?b ; \<lbrakk>?b = base_for_lit ?l;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 , ?v2.0 ]\<^sup>v : ?b ; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b1 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons ?tyid ?dc ?v : ?b ; \<And>dclist x b' c. \<lbrakk>?b = B_id ?tyid; AF_typedef ?tyid dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b' \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp ?tyid ?dc ?b ?v : ?b' ; \<And>bv dclist x b' c. \<lbrakk>?b' = B_app ?tyid ?b; AF_typedef_poly ?tyid bv dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; atom bv \<sharp> (?\<Theta>, ?\<B>, ?\<Gamma>, ?b, ?v);  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b'[bv::=?b]\<^sub>b\<^sub>b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1. (\<And>c1. Some (b, c1) = lookup \<Gamma> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Some (b, c1) = lookup \<Gamma> x

goal (4 subgoals):
 1. \<And>x s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 4. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Some s = i x \<and> Some s' = i' x
Some (b, c1) = lookup \<Gamma> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Some s = i x \<and> Some s' = i' x
Some (b, c1) = lookup \<Gamma> x

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using bs_boxed_var V_var
[PROOF STATE]
proof (prove)
using this:
Some s = i x \<and> Some s' = i' x
Some (b, c1) = lookup \<Gamma> x
\<lbrakk> ?\<Theta>  ; ?\<Gamma> ; ?b' , ?bv \<turnstile> ?i \<approx> ?i'; Some (?b, ?c) = lookup ?\<Gamma> ?x; Some ?s = ?i ?x; Some ?s' = ?i' ?x\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> ?s ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ x ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

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

goal (3 subgoals):
 1. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
case (V_pair v1 v2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ v1 , v2 ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (3 subgoals):
 1. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ v1 , v2 ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'
[PROOF STEP]
obtain b1 and b2 where b:"b=B_pair b1 b2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ v1 , v2 ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1. (\<And>b1 b2. b = [ b1 , b2 ]\<^sup>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfV_elims subst_vb.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ v1 , v2 ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?x ]\<^sup>v : ?b ; \<And>c. \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; Some (?b, c) = lookup ?\<Gamma> ?x\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : ?b ; \<lbrakk>?b = base_for_lit ?l;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 , ?v2.0 ]\<^sup>v : ?b ; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b1 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons ?tyid ?dc ?v : ?b ; \<And>dclist x b' c. \<lbrakk>?b = B_id ?tyid; AF_typedef ?tyid dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b' \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp ?tyid ?dc ?b ?v : ?b' ; \<And>bv dclist x b' c. \<lbrakk>?b' = B_app ?tyid ?b; AF_typedef_poly ?tyid bv dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; atom bv \<sharp> (?\<Theta>, ?\<B>, ?\<Gamma>, ?b, ?v);  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b'[bv::=?b]\<^sub>b\<^sub>b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?y ]\<^sup>v
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>b = V_cons ?tyid ?c (?v'[?x::=?v]\<^sub>v\<^sub>b)
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>b = V_consp ?tyid ?c ?b[?x::=?v]\<^sub>b\<^sub>b (?v'[?x::=?v]\<^sub>v\<^sub>b)
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>b , ?v2.0[?x::=?v]\<^sub>v\<^sub>b ]\<^sup>v

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

goal (3 subgoals):
 1. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
obtain s1 and s2 where s: "eval_v i (v1[bv::=b']\<^sub>v\<^sub>b) s1 \<and> eval_v i (v2[bv::=b']\<^sub>v\<^sub>b) s2 \<and> s = SPair s1 s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2  \<and> s = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_pair subst_vb.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ v1 , v2 ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?y ]\<^sup>v
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>b = V_cons ?tyid ?c (?v'[?x::=?v]\<^sub>v\<^sub>b)
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>b = V_consp ?tyid ?c ?b[?x::=?v]\<^sub>b\<^sub>b (?v'[?x::=?v]\<^sub>v\<^sub>b)
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>b , ?v2.0[?x::=?v]\<^sub>v\<^sub>b ]\<^sup>v

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2  \<and> s = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2  \<and> s = SPair s1 s2

goal (3 subgoals):
 1. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
obtain s1' and s2' where s': "eval_v i' v1 s1' \<and> eval_v i' v2 s2' \<and> s' = SPair s1' s2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1' s2'. i' \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i' \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_pair
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ v1 , v2 ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1. (\<And>s1' s2'. i' \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i' \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i' \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i' \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'

goal (3 subgoals):
 1. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
have  "boxed_b  \<Theta> (SPair s1 s2) (B_pair b1 b2)  bv b' (SPair s1' s2') "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> SPair s1 s2 ~ [ b1 , b2 ]\<^sup>b [ bv ::= b' ] \<setminus> SPair s1' s2'
[PROOF STEP]
proof(rule boxed_b_BPairI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  \<Theta>  \<turnstile> s1 ~ b1 [ bv ::= b' ] \<setminus> s1'
 2.  \<Theta>  \<turnstile> s2 ~ b2 [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
show "boxed_b \<Theta> s1 b1 bv b' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s1 ~ b1 [ bv ::= b' ] \<setminus> s1'
[PROOF STEP]
using V_pair eval_v_elims wfV_elims b s s' b.eq_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ v1 , v2 ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?x ]\<^sup>v : ?b ; \<And>c. \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; Some (?b, c) = lookup ?\<Gamma> ?x\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : ?b ; \<lbrakk>?b = base_for_lit ?l;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 , ?v2.0 ]\<^sup>v : ?b ; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b1 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons ?tyid ?dc ?v : ?b ; \<And>dclist x b' c. \<lbrakk>?b = B_id ?tyid; AF_typedef ?tyid dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b' \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp ?tyid ?dc ?b ?v : ?b' ; \<And>bv dclist x b' c. \<lbrakk>?b' = B_app ?tyid ?b; AF_typedef_poly ?tyid bv dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; atom bv \<sharp> (?\<Theta>, ?\<B>, ?\<Gamma>, ?b, ?v);  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b'[bv::=?b]\<^sub>b\<^sub>b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
b = [ b1 , b2 ]\<^sup>b
i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2  \<and> s = SPair s1 s2
i' \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i' \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'
(B_int = B_int) = True
(B_bool = B_bool) = True
(B_id ?list = B_id ?lista) = (?list = ?lista)
([ ?b1.0 , ?b2.0 ]\<^sup>b = [ ?b1a , ?b2a ]\<^sup>b) = (?b1.0 = ?b1a \<and> ?b2.0 = ?b2a)
(B_unit = B_unit) = True
(B_bitvec = B_bitvec) = True
(B_var ?bv = B_var ?bva) = (?bv = ?bva)
(B_app ?list ?b = B_app ?lista ?ba) = (?list = ?lista \<and> ?b = ?ba)

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

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s2 ~ b2 [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
show "boxed_b \<Theta> s2 b2 bv b' s2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s2 ~ b2 [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
using V_pair eval_v_elims wfV_elims b s s' b.eq_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> [ v1 , v2 ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b
 \<Theta> ; \<Gamma> \<turnstile> i'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?x ]\<^sup>v : ?b ; \<And>c. \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; Some (?b, c) = lookup ?\<Gamma> ?x\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : ?b ; \<lbrakk>?b = base_for_lit ?l;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 , ?v2.0 ]\<^sup>v : ?b ; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b1 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons ?tyid ?dc ?v : ?b ; \<And>dclist x b' c. \<lbrakk>?b = B_id ?tyid; AF_typedef ?tyid dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b' \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp ?tyid ?dc ?b ?v : ?b' ; \<And>bv dclist x b' c. \<lbrakk>?b' = B_app ?tyid ?b; AF_typedef_poly ?tyid bv dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; atom bv \<sharp> (?\<Theta>, ?\<B>, ?\<Gamma>, ?b, ?v);  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b'[bv::=?b]\<^sub>b\<^sub>b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
b = [ b1 , b2 ]\<^sup>b
i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2  \<and> s = SPair s1 s2
i' \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i' \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'
(B_int = B_int) = True
(B_bool = B_bool) = True
(B_id ?list = B_id ?lista) = (?list = ?lista)
([ ?b1.0 , ?b2.0 ]\<^sup>b = [ ?b1a , ?b2a ]\<^sup>b) = (?b1.0 = ?b1a \<and> ?b2.0 = ?b2a)
(B_unit = B_unit) = True
(B_bitvec = B_bitvec) = True
(B_var ?bv = B_var ?bva) = (?bv = ?bva)
(B_app ?list ?b = B_app ?lista ?ba) = (?list = ?lista \<and> ?b = ?ba)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 \<Theta>  \<turnstile> SPair s1 s2 ~ [ b1 , b2 ]\<^sup>b [ bv ::= b' ] \<setminus> SPair s1' s2'

goal (3 subgoals):
 1. \<And>x1a x2a s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x1a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x1a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; \<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x2a[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x2a \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> [ x1a , x2a ]\<^sup>v[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 3. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta>  \<turnstile> SPair s1 s2 ~ [ b1 , b2 ]\<^sup>b [ bv ::= b' ] \<setminus> SPair s1' s2'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile> SPair s1 s2 ~ [ b1 , b2 ]\<^sup>b [ bv ::= b' ] \<setminus> SPair s1' s2'

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using s s' b
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile> SPair s1 s2 ~ [ b1 , b2 ]\<^sup>b [ bv ::= b' ] \<setminus> SPair s1' s2'
i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2  \<and> s = SPair s1 s2
i' \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i' \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'
b = [ b1 , b2 ]\<^sup>b

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

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
case (V_cons tyid dc v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> (V_cons tyid dc v1)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons tyid dc v1 : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
obtain dclist x b1 c where *: "b = B_id tyid \<and> AF_typedef tyid dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>dclist x b1 c. b = B_id tyid \<and> AF_typedef tyid dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfV_elims(4)[OF V_cons(5)] V_cons
[PROOF STATE]
proof (prove)
using this:
(\<And>dclist x b' c. \<lbrakk>b = B_id tyid; AF_typedef tyid dclist \<in> set \<Theta>; (dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b' \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> (V_cons tyid dc v1)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons tyid dc v1 : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1. (\<And>dclist x b1 c. b = B_id tyid \<and> AF_typedef tyid dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b = B_id tyid \<and> AF_typedef tyid dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
obtain s2 where s2: "s = SCons tyid dc s2 \<and>  i \<lbrakk> (v1[bv::=b']\<^sub>v\<^sub>b) \<rbrakk> ~ s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s2. s = SCons tyid dc s2 \<and> i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_cons subst_vb.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> (V_cons tyid dc v1)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons tyid dc v1 : b
 \<Theta> ; \<Gamma> \<turnstile> i'
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?y ]\<^sup>v
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>b = V_cons ?tyid ?c (?v'[?x::=?v]\<^sub>v\<^sub>b)
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>b = V_consp ?tyid ?c ?b[?x::=?v]\<^sub>b\<^sub>b (?v'[?x::=?v]\<^sub>v\<^sub>b)
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>b , ?v2.0[?x::=?v]\<^sub>v\<^sub>b ]\<^sup>v

goal (1 subgoal):
 1. (\<And>s2. s = SCons tyid dc s2 \<and> i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = SCons tyid dc s2 \<and> i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
obtain s2' where s2': "s' = SCons tyid dc s2' \<and>  i' \<lbrakk> v1 \<rbrakk> ~ s2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s2'. s' = SCons tyid dc s2' \<and> i' \<lbrakk> v1 \<rbrakk> ~ s2'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> (V_cons tyid dc v1)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons tyid dc v1 : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1. (\<And>s2'. s' = SCons tyid dc s2' \<and> i' \<lbrakk> v1 \<rbrakk> ~ s2'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s' = SCons tyid dc s2' \<and> i' \<lbrakk> v1 \<rbrakk> ~ s2'

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
have sp: "supp \<lbrace> x : b1  | c \<rbrace> = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp \<lbrace> x : b1  | c \<rbrace> = {}
[PROOF STEP]
using wfTh_lookup_supp_empty * wfX_wfY
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>AF_typedef ?tid ?dclist \<in> set ?\<Theta>; (?c, ?t) \<in> set ?dclist;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta> \<rbrakk> \<Longrightarrow> supp ?t = {}
b = B_id tyid \<and> AF_typedef tyid dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f b_of ?\<tau>
 ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ts  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> True
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ce : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> \<turnstile>\<^sub>w\<^sub>f ?td  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?e : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?css : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f ?ftq  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> \<turnstile>\<^sub>w\<^sub>f ?ft  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>

goal (1 subgoal):
 1. supp \<lbrace> x : b1  | c \<rbrace> = {}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
supp \<lbrace> x : b1  | c \<rbrace> = {}

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
have "boxed_b \<Theta> (SCons tyid dc s2) (B_id tyid) bv b' (SCons tyid dc s2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> SCons tyid dc s2 ~ B_id tyid [ bv ::= b' ] \<setminus> SCons tyid dc s2'
[PROOF STEP]
proof(rule boxed_b_BConsI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. AF_typedef tyid ?dclist \<in> set \<Theta>
 2. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist
 3.  \<Theta>  \<turnstile> s2 ~ ?b [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
show 1:"AF_typedef tyid dclist \<in> set \<Theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AF_typedef tyid dclist \<in> set \<Theta>
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
b = B_id tyid \<and> AF_typedef tyid dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1

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

goal (2 subgoals):
 1. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set dclist
 2.  \<Theta>  \<turnstile> s2 ~ ?b [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
show 2:"(dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
b = B_id tyid \<and> AF_typedef tyid dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1

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

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s2 ~ b1 [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
have bvf:"atom bv \<sharp> b1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom bv \<sharp> b1
[PROOF STEP]
using sp  \<tau>.fresh fresh_def
[PROOF STATE]
proof (prove)
using this:
supp \<lbrace> x : b1  | c \<rbrace> = {}
?a \<sharp> \<lbrace> ?x : ?b  | ?c \<rbrace> = ((?a \<sharp> ?c \<or> ?a \<in> set [atom ?x]) \<and> ?a \<sharp> ?b)
?a \<sharp> ?x \<equiv> ?a \<notin> supp ?x

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

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s2 ~ b1 [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
show "\<Theta>  \<turnstile> s2 ~ b1 [ bv ::= b' ] \<setminus> s2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s2 ~ b1 [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
using V_cons s2 s2' *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> (V_cons tyid dc v1)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons tyid dc v1 : b
 \<Theta> ; \<Gamma> \<turnstile> i'
s = SCons tyid dc s2 \<and> i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2
s' = SCons tyid dc s2' \<and> i' \<lbrakk> v1 \<rbrakk> ~ s2'
b = B_id tyid \<and> AF_typedef tyid dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1

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

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

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x3[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_cons x1a x2a x3)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta>  \<turnstile> SCons tyid dc s2 ~ B_id tyid [ bv ::= b' ] \<setminus> SCons tyid dc s2'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile> SCons tyid dc s2 ~ B_id tyid [ bv ::= b' ] \<setminus> SCons tyid dc s2'

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using * s2 s2'
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile> SCons tyid dc s2 ~ B_id tyid [ bv ::= b' ] \<setminus> SCons tyid dc s2'
b = B_id tyid \<and> AF_typedef tyid dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x : b1  | c \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1
s = SCons tyid dc s2 \<and> i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2
s' = SCons tyid dc s2' \<and> i' \<lbrakk> v1 \<rbrakk> ~ s2'

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

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
case (V_consp tyid dc b1 v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> (V_consp tyid dc b1 v1)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp tyid dc b1 v1 : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
obtain bv2 dclist x2 b2 c2 where *: "b = B_app tyid b1 \<and> AF_typedef_poly tyid bv2 dclist \<in> set \<Theta> \<and>
       (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b2[bv2::=b1]\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bv2 dclist x2 b2 c2. b = B_app tyid b1 \<and> AF_typedef_poly tyid bv2 dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b2[bv2::=b1]\<^sub>b\<^sub>b  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wf_strong_elim(1)[OF V_consp (5)]
[PROOF STATE]
proof (prove)
using this:
\<exists>bv dclist x b' c. b = B_app tyid b1 \<and> AF_typedef_poly tyid bv dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f b1  \<and> atom bv \<sharp> (\<Theta>, B, \<Gamma>, b1, v1) \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b'[bv::=b1]\<^sub>b\<^sub>b  \<and> atom bv \<sharp> ?tm

goal (1 subgoal):
 1. (\<And>bv2 dclist x2 b2 c2. b = B_app tyid b1 \<and> AF_typedef_poly tyid bv2 dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b2[bv2::=b1]\<^sub>b\<^sub>b  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b = B_app tyid b1 \<and> AF_typedef_poly tyid bv2 dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b2[bv2::=b1]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
obtain s2 where s2: "s = SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2 \<and>  i \<lbrakk> (v1[bv::=b']\<^sub>v\<^sub>b) \<rbrakk> ~ s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s2. s = SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2 \<and> i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_consp subst_vb.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> (V_consp tyid dc b1 v1)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp tyid dc b1 v1 : b
 \<Theta> ; \<Gamma> \<turnstile> i'
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?y ]\<^sup>v
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>b = V_cons ?tyid ?c (?v'[?x::=?v]\<^sub>v\<^sub>b)
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>b = V_consp ?tyid ?c ?b[?x::=?v]\<^sub>b\<^sub>b (?v'[?x::=?v]\<^sub>v\<^sub>b)
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>b = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>b , ?v2.0[?x::=?v]\<^sub>v\<^sub>b ]\<^sup>v

goal (1 subgoal):
 1. (\<And>s2. s = SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2 \<and> i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2 \<and> i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
obtain s2' where s2': "s' = SConsp tyid dc b1 s2' \<and>  i' \<lbrakk> v1 \<rbrakk> ~ s2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s2'. s' = SConsp tyid dc b1 s2' \<and> i' \<lbrakk> v1 \<rbrakk> ~ s2'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_consp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> (V_consp tyid dc b1 v1)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp tyid dc b1 v1 : b
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1. (\<And>s2'. s' = SConsp tyid dc b1 s2' \<and> i' \<lbrakk> v1 \<rbrakk> ~ s2'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s' = SConsp tyid dc b1 s2' \<and> i' \<lbrakk> v1 \<rbrakk> ~ s2'

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
have "\<turnstile>\<^sub>w\<^sub>f \<Theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
[PROOF STEP]
using V_consp wfX_wfY
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> (V_consp tyid dc b1 v1)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp tyid dc b1 v1 : b
 \<Theta> ; \<Gamma> \<turnstile> i'
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f b_of ?\<tau>
 ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ts  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> True
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ce : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> \<turnstile>\<^sub>w\<^sub>f ?td  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?e : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?css : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f ?ftq  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> \<turnstile>\<^sub>w\<^sub>f ?ft  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>

goal (1 subgoal):
 1.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
[PROOF STEP]
obtain bv3::bv and dclist3 x3 b3 c3 where **:" AF_typedef_poly tyid bv2 dclist =  AF_typedef_poly tyid bv3 dclist3 \<and>
        (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3 \<and> atom bv3 \<sharp> (b1, bv, b', s2, s2') \<and> b2[bv2::=b1]\<^sub>b\<^sub>b = b3[bv3::=b1]\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>

goal (1 subgoal):
 1. (\<And>bv3 dclist3 x3 b3 c3. AF_typedef_poly tyid bv2 dclist = AF_typedef_poly tyid bv3 dclist3 \<and> (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3 \<and> atom bv3 \<sharp> (b1, bv, b', s2, s2') \<and> b2[bv2::=b1]\<^sub>b\<^sub>b = b3[bv3::=b1]\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using * obtain_fresh_bv_dclist_b_iff[where tm="(b1, bv, b', s2, s2')"]
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
b = B_app tyid b1 \<and> AF_typedef_poly tyid bv2 dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b2[bv2::=b1]\<^sub>b\<^sub>b
\<lbrakk>(?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; AF_typedef_poly ?tyid ?bv ?dclist \<in> set ?P;    \<turnstile>\<^sub>w\<^sub>f ?P ; \<And>bv1 dclist1 x1 b1a c1. AF_typedef_poly ?tyid ?bv ?dclist = AF_typedef_poly ?tyid bv1 dclist1 \<and> (?dc, \<lbrace> x1 : b1a  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> (b1, bv, b', s2, s2') \<and> ?b[?bv::=?b']\<^sub>b\<^sub>b = b1a[bv1::=?b']\<^sub>b\<^sub>b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>bv3 dclist3 x3 b3 c3. AF_typedef_poly tyid bv2 dclist = AF_typedef_poly tyid bv3 dclist3 \<and> (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3 \<and> atom bv3 \<sharp> (b1, bv, b', s2, s2') \<and> b2[bv2::=b1]\<^sub>b\<^sub>b = b3[bv3::=b1]\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bv2 dclist = AF_typedef_poly tyid bv3 dclist3 \<and> (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3 \<and> atom bv3 \<sharp> (b1, bv, b', s2, s2') \<and> b2[bv2::=b1]\<^sub>b\<^sub>b = b3[bv3::=b1]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
have "boxed_b \<Theta> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2) (B_app tyid b1) bv b' (SConsp tyid dc b1 s2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> SConsp tyid dc b1 s2'
[PROOF STEP]
proof(rule boxed_b_BConspI[of tyid bv3 dclist3 \<Theta>, where x=x3 and b=b3 and c=c3])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. AF_typedef_poly tyid bv3 dclist3 \<in> set \<Theta>
 2. atom bv3 \<sharp> (b1, bv, b', s2, s2')
 3. (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3
 4.  \<Theta>  \<turnstile> s2 ~ b3[bv3::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
show 1:"AF_typedef_poly tyid bv3 dclist3 \<in> set \<Theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AF_typedef_poly tyid bv3 dclist3 \<in> set \<Theta>
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
b = B_app tyid b1 \<and> AF_typedef_poly tyid bv2 dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b2[bv2::=b1]\<^sub>b\<^sub>b
AF_typedef_poly tyid bv2 dclist = AF_typedef_poly tyid bv3 dclist3 \<and> (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3 \<and> atom bv3 \<sharp> (b1, bv, b', s2, s2') \<and> b2[bv2::=b1]\<^sub>b\<^sub>b = b3[bv3::=b1]\<^sub>b\<^sub>b

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

goal (3 subgoals):
 1. atom bv3 \<sharp> (b1, bv, b', s2, s2')
 2. (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3
 3.  \<Theta>  \<turnstile> s2 ~ b3[bv3::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
show 2:"(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv2 dclist = AF_typedef_poly tyid bv3 dclist3 \<and> (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3 \<and> atom bv3 \<sharp> (b1, bv, b', s2, s2') \<and> b2[bv2::=b1]\<^sub>b\<^sub>b = b3[bv3::=b1]\<^sub>b\<^sub>b

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

goal (2 subgoals):
 1. atom bv3 \<sharp> (b1, bv, b', s2, s2')
 2.  \<Theta>  \<turnstile> s2 ~ b3[bv3::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
show "atom bv3 \<sharp> (b1, bv, b', s2, s2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom bv3 \<sharp> (b1, bv, b', s2, s2')
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv2 dclist = AF_typedef_poly tyid bv3 dclist3 \<and> (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3 \<and> atom bv3 \<sharp> (b1, bv, b', s2, s2') \<and> b2[bv2::=b1]\<^sub>b\<^sub>b = b3[bv3::=b1]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. atom bv3 \<sharp> (b1, bv, b', s2, s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom bv3 \<sharp> (b1, bv, b', s2, s2')

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s2 ~ b3[bv3::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
show " \<Theta>  \<turnstile> s2 ~ b3[bv3::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s2 ~ b3[bv3::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
using V_consp s2 s2' * **
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ ?s ; i' \<lbrakk> v1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> ?s ~ ?b [ bv ::= b' ] \<setminus> ?s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
i \<lbrakk> (V_consp tyid dc b1 v1)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s
i' \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp tyid dc b1 v1 : b
 \<Theta> ; \<Gamma> \<turnstile> i'
s = SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2 \<and> i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2
s' = SConsp tyid dc b1 s2' \<and> i' \<lbrakk> v1 \<rbrakk> ~ s2'
b = B_app tyid b1 \<and> AF_typedef_poly tyid bv2 dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b2[bv2::=b1]\<^sub>b\<^sub>b
AF_typedef_poly tyid bv2 dclist = AF_typedef_poly tyid bv3 dclist3 \<and> (dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3 \<and> atom bv3 \<sharp> (b1, bv, b', s2, s2') \<and> b2[bv2::=b1]\<^sub>b\<^sub>b = b3[bv3::=b1]\<^sub>b\<^sub>b

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s2 ~ b3[bv3::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 \<Theta>  \<turnstile> s2 ~ b3[bv3::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2'

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

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s' b. \<lbrakk>\<And>s s' b. \<lbrakk> \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> x4[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; i \<lbrakk> (V_consp x1a x2a x3 x4)[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s ; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b ;  \<Theta> ; \<Gamma> \<turnstile> i'\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta>  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> SConsp tyid dc b1 s2'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> SConsp tyid dc b1 s2'

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using * s2 s2'
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile> SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> SConsp tyid dc b1 s2'
b = B_app tyid b1 \<and> AF_typedef_poly tyid bv2 dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist \<and>  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b2[bv2::=b1]\<^sub>b\<^sub>b
s = SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s2 \<and> i \<lbrakk> v1[bv::=b']\<^sub>v\<^sub>b \<rbrakk> ~ s2
s' = SConsp tyid dc b1 s2' \<and> i' \<lbrakk> v1 \<rbrakk> ~ s2'

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

goal:
No subgoals!
[PROOF STEP]
qed