Theory IVSubstTypingL

(*<*)
theory IVSubstTypingL
  imports  SubstMethods ContextSubtypingL
begin
  (*>*)

chapter ‹Immutable Variable Substitution Lemmas›
text ‹Lemmas that show that types are preserved, in some way, 
under immutable variable substitution›

section ‹Proof Methods›

method subst_mth = (metis  subst_g_inside  infer_e_wf infer_v_wf infer_v_wf)

method subst_tuple_mth uses add = (
    (unfold fresh_prodN), (simp add: add  )+,
    (rule,metis fresh_z_subst_g add fresh_Pair ),
    (metis fresh_subst_dv add fresh_Pair ) )

section ‹Prelude›

lemma subst_top_eq:
  "⦃ z : b  | TRUE ⦄ = ⦃ z : b  | TRUE ⦄[x::=v]τv" 
proof -
  obtain z'::x and c' where zeq: "⦃ z : b  | TRUE ⦄ = ⦃ z' : b | c' ⦄ ∧ atom z' ♯ (x,v)" using obtain_fresh_z2 b_of.simps by metis
  hence "⦃ z' : b  | TRUE ⦄[x::=v]τv =  ⦃ z' : b | TRUE ⦄" using subst_tv.simps subst_cv.simps by metis
  moreover have "c' = C_true" using τ.eq_iff Abs1_eq_iff(3) c.fresh flip_fresh_fresh  by (metis zeq) 
  ultimately show ?thesis using zeq by metis
qed

lemma wfD_subst:
  fixes τ1::τ and v::v and Δ::Δ and Θ::Θ and Γ::Γ
  assumes "Θ ; ℬ ; Γ ⊢ v ⇒ τ1" and "wfD Θ  ℬ (Γ'@((x,b1,c0[z0::=[x]v]cv) #Γ Γ))  Δ" and "b_of τ1=b1"
  shows " Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢wf Δ[x::=v]Δv"
proof -
  have "Θ ; ℬ ; Γ⊢wf v : b1" using infer_v_v_wf assms by auto
  moreover have  "(Γ'@((x,b1,c0[z0::=[x]v]cv)#ΓΓ))[x::=v]Γv = Γ'[x::=v]Γv @ Γ"  using subst_g_inside wfD_wf  assms by metis
  ultimately show ?thesis  using  wf_subst assms by metis
qed

lemma subst_v_c_of:
  assumes  "atom xa ♯ (v,x)"
  shows  "c_of t[x::=v]τv xa = (c_of t xa)[x::=v]cv" 
  using assms proof(nominal_induct t avoiding: x v xa rule:τ.strong_induct)
  case (T_refined_type z' b' c')
  then have " c_of ⦃ z' : b'  | c' ⦄[x::=v]τv xa  = c_of ⦃ z' : b'  | c'[x::=v]cv ⦄ xa" 
    using subst_tv.simps fresh_Pair by metis
  also have "... =  c'[x::=v]cv [z'::=V_var xa]cv" using c_of.simps T_refined_type by metis
  also have "... = c' [z'::=V_var xa]cv[x::=v]cv" 
    using subst_cv_commute_full[of z' v x "V_var xa" c'] subst_v_c_def T_refined_type fresh_Pair fresh_at_base v.fresh fresh_x_neq by metis
  finally show ?case using c_of.simps T_refined_type by metis  
qed

section ‹Context›

lemma subst_lookup:
  assumes "Some (b,c) = lookup (Γ'@((x,b1,c1)#ΓΓ)) y" and "x ≠ y" and "wfG Θ ℬ (Γ'@((x,b1,c1)#ΓΓ))"
  shows "∃d. Some (b,d) = lookup ((Γ'[x::=v]Γv)@Γ) y" 
  using assms proof(induct Γ' rule: Γ_induct)
  case GNil
  hence "Some (b,c) = lookup Γ y"     by (simp add: assms(1))
  then show ?case using subst_gv.simps by auto
next
  case (GCons x1 b1 c1  Γ1)
  show ?case proof(cases "x1 = x")
    case True
    hence "atom x ♯ (Γ1 @ (x, b1, c1) #Γ Γ)" using GCons wfG_elims(2)
        append_g.simps  by metis
    moreover have  "atom x ∈ atom_dom (Γ1 @ (x, b1, c1) #Γ Γ)" by simp
    ultimately show ?thesis 
      using forget_subst_gv  not_GCons_self2 subst_gv.simps append_g.simps  
      by (metis GCons.prems(3) True wfG_cons_fresh2 )
  next
    case False
    hence "((x1,b1,c1) #Γ Γ1)[x::=v]Γv = (x1,b1,c1[x::=v]cv)#ΓΓ1[x::=v]Γv"  using subst_gv.simps by auto
    then show ?thesis  proof(cases "x1=y")
      case True
      then show ?thesis using GCons  using lookup.simps 
        by (metis ‹((x1, b1, c1) #Γ Γ1)[x::=v]Γv = (x1, b1, c1[x::=v]cv) #Γ Γ1[x::=v]Γv› append_g.simps fst_conv option.inject)
    next
      case False
      then show ?thesis using GCons  using lookup.simps 
        using ‹((x1, b1, c1) #Γ Γ1)[x::=v]Γv = (x1, b1, c1[x::=v]cv) #Γ Γ1[x::=v]Γv› append_g.simps Γ.distinct Γ.inject wfG.simps wfG_elims by metis        
    qed
  qed
qed

section ‹Validity›

lemma subst_self_valid: 
  fixes v::v
  assumes  "Θ ; ℬ ; G ⊢ v ⇒ ⦃ z : b | c ⦄" and "atom z ♯ v"
  shows " Θ ; ℬ ; G ⊨ c[z::=v]cv"
proof - 
  have "c= (CE_val (V_var z)  ==  CE_val v )" using  infer_v_form2 assms by presburger
  hence "c[z::=v]cv = (CE_val (V_var z)  ==  CE_val v )[z::=v]cv" by auto
  also have "... = (((CE_val (V_var z))[z::=v]cev) ==  ((CE_val v)[z::=v]cev))" by fastforce
  also have "... = ((CE_val v) ==  ((CE_val v)[z::=v]cev))" using subst_cev.simps subst_vv.simps by presburger
  also have "... = (CE_val v  ==  CE_val v )" using infer_v_form subst_cev.simps assms forget_subst_vv   by presburger
  finally have *:"c[z::=v]cv = (CE_val v  ==  CE_val v )" by auto

  have **:"Θ ; ℬ ; G⊢wf CE_val v : b" using wfCE_valI  assms infer_v_v_wf b_of.simps by metis

  show ?thesis proof(rule validI)
    show  "Θ ; ℬ ; G⊢wf c[z::=v]cv" proof -
      have "Θ ; ℬ ; G⊢wf v : b" using infer_v_v_wf assms b_of.simps by metis
      moreover have "Θ ⊢wf ([]::Φ)    ∧  Θ ; ℬ ; G⊢wf []Δ" using wfD_emptyI wfPhi_emptyI infer_v_wf assms by auto
      ultimately show ?thesis using * wfCE_valI wfC_eqI by metis
    qed
    show "∀i. wfI Θ G i ∧ is_satis_g i G ⟶ is_satis i c[z::=v]cv" proof(rule,rule)
      fix i 
      assume ‹wfI Θ G i ∧ is_satis_g i G›
      thus ‹is_satis i c[z::=v]cv› using * ** is_satis_eq by auto
    qed
  qed
qed

lemma subst_valid_simple: 
  fixes v::v
  assumes "Θ ; ℬ ; G ⊢ v ⇒ ⦃ z0 : b | c0 ⦄" and 
    "atom z0 ♯ c" and "atom z0 ♯ v"
    "Θ; ℬ ; (z0,b,c0)#ΓG ⊨ c[z::=V_var z0]cv" 
  shows " Θ ; ℬ ; G ⊨ c[z::=v]cv"
proof -
  have " Θ ; ℬ ; G ⊨ c0[z0::=v]cv"  using subst_self_valid assms by metis
  moreover have "atom z0 ♯ G" using assms valid_wf_all by meson
  moreover  have "wfV Θ ℬ G v b" using infer_v_v_wf assms b_of.simps by metis
  moreover have "(c[z::=V_var z0]cv)[z0::=v]cv = c[z::=v]cv" using subst_v_simple_commute assms subst_v_c_def by metis
  ultimately show ?thesis  using valid_trans assms subst_defs by metis
qed

lemma wfI_subst1:
  assumes " wfI Θ (G'[x::=v]Γv @ G) i" and "wfG Θ ℬ (G' @ (x, b, c[z::=[x]v]cv) #Γ G)" and "eval_v i v sv" and "wfRCV Θ sv b"
  shows "wfI Θ (G' @ (x, b, c[z::=[x]v]cv) #Γ G) ( i( x ↦ sv))"
proof - 
  {
    fix xa::x and ba::b  and ca::c
    assume as: "(xa,ba,ca) ∈ toSet ((G' @ ((x, b, c[z::=[x]v]cv) #Γ G)))"
    then have " ∃s. Some s = (i(x ↦ sv)) xa ∧ wfRCV Θ s ba"
    proof(cases "x=xa") 
      case True
      have "Some sv =  (i(x ↦ sv)) x ∧ wfRCV Θ sv b" using as assms wfI_def by auto
      moreover have "b=ba" using  assms as True wfG_member_unique by metis
      ultimately show ?thesis using True by auto
    next
      case False

      then obtain ca' where "(xa, ba, ca') ∈ toSet (G'[x::=v]Γv @ G)" using wfG_member_subst2 assms as by metis
      then obtain s where " Some s = i xa ∧ wfRCV Θ s ba" using wfI_def assms False by blast
      thus  ?thesis using False by auto
    qed   
  }
  from this show ?thesis using wfI_def allI by blast 
qed

lemma subst_valid:
  fixes v::v and c'::c and Γ ::Γ
  assumes "Θ ; ℬ ; Γ ⊨ c[z::=v]cv" and  "Θ ; ℬ ; Γ⊢wf v : b" and 
    "Θ ; ℬ⊢wf Γ" and  "atom x ♯ c" and  "atom x ♯ Γ" and 
    "Θ ; ℬ⊢wf (Γ'@(x,b,c[z::=[x]v]cv ) #Γ Γ)" and          
    "Θ ; ℬ ; Γ'@(x,b, c[z::=[x]v]cv ) #Γ Γ ⊨ c'" (is " Θ ; ℬ;  ?G ⊨ c'")
  shows   "Θ ; ℬ ; Γ'[x::=v]Γv@Γ ⊨ c'[x::=v]cv"
proof -
  have *:"wfC Θ ℬ (Γ'@(x,b, c[z::=[x]v]cv ) #Γ Γ) c'"  using valid.simps assms by metis
  hence "wfC Θ ℬ (Γ'[x::=v]Γv @ Γ) (c'[x::=v]cv)" using wf_subst(2)[OF *]  b_of.simps   assms subst_g_inside wfC_wf  by metis
  moreover have "∀i. wfI Θ (Γ'[x::=v]Γv @ Γ) i ∧ is_satis_g i (Γ'[x::=v]Γv @ Γ) ⟶ is_satis i (c'[x::=v]cv)" 

  proof(rule,rule)
    fix i
    assume as: " wfI Θ (Γ'[x::=v]Γv @ Γ) i ∧ is_satis_g i (Γ'[x::=v]Γv @ Γ)"

    hence wfig: "wfI Θ Γ i" using wfI_suffix infer_v_wf assms by metis 
    then obtain s where s:"eval_v i v s" and b:"wfRCV Θ s b" using eval_v_exist infer_v_v_wf b_of.simps assms by metis

    have is1: "is_satis_g ( i( x ↦ s)) (Γ' @ (x, b, c[z::=[x]v]cv) #Γ Γ)" proof(rule is_satis_g_i_upd2)
      show "is_satis (i(x ↦ s)) (c[z::=[x]v]cv)" proof - 
        have "is_satis i  (c[z::=v]cv)" 
          using subst_valid_simple assms as valid.simps infer_v_wf assms
            is_satis_g_suffix wfI_suffix by metis
        hence "is_satis i ((c[z::=[x]v]cv)[x::=v]cv)" using assms subst_v_simple_commute[of x c z v] subst_v_c_def by metis
        moreover have "Θ ; ℬ ; (x, b, c[z::=[x]v]cv) #Γ Γ ⊢wf c[z::=[x]v]cv" using wfC_refl wfG_suffix assms by metis
        moreover have "Θ ; ℬ ; Γ⊢wf v : b" using assms infer_v_v_wf b_of.simps by metis
        ultimately show ?thesis using subst_c_satis[OF s , of Θ ℬ x b  "c[z::=[x]v]cv" Γ "c[z::=[x]v]cv"] wfig by auto
      qed        
      show "atom x ♯ Γ" using assms by metis
      show "wfG Θ ℬ (Γ' @ (x, b, c[z::=[x]v]cv) #Γ Γ)" using valid_wf_all assms by metis
      show "Θ ; ℬ ; Γ⊢wf v : b" using assms infer_v_v_wf by force
      show "i ⟦ v ⟧ ~ s " using s by auto
      show "Θ ; Γ'[x::=v]Γv @ Γ ⊢ i" using as by auto
      show "i ⊨ Γ'[x::=v]Γv @ Γ " using as by auto
    qed
    hence "is_satis ( i( x ↦ s)) c'" proof -
      have "wfI  Θ (Γ' @ (x, b, c[z::=[x]v]cv) #Γ Γ) ( i( x ↦ s))" 
        using wfI_subst1[of Θ Γ' x v  Γ i ℬ b c z  s] as b s assms  by metis
      thus ?thesis using is1 valid.simps assms by presburger
    qed

    thus "is_satis i (c'[x::=v]cv)" using subst_c_satis_full[OF s] valid.simps as infer_v_v_wf b_of.simps assms by metis 

  qed
  ultimately show ?thesis using valid.simps by auto
qed

lemma subst_valid_infer_v:
  fixes v::v and c'::c
  assumes  "Θ ; ℬ ; G ⊢ v ⇒ ⦃ z0 : b | c0 ⦄" and  "atom x ♯ c" and  "atom x ♯ G" and "wfG Θ ℬ (G'@(x,b,c[z::=[x]v]cv ) #Γ G)" and "atom z0 ♯ v"
    " Θ;ℬ;(z0,b,c0)#ΓG ⊨ c[z::=V_var z0]cv" and "atom z0 ♯ c" and
    " Θ;ℬ;G'@(x,b, c[z::=[x]v]cv ) #Γ G ⊨ c'" (is " Θ ; ℬ;  ?G ⊨ c'")
  shows    " Θ;ℬ;G'[x::=v]Γv@G ⊨ c'[x::=v]cv"
proof - 
  have "Θ ; ℬ ; G ⊨ c[z::=v]cv"  
    using infer_v_wf subst_valid_simple valid.simps assms    using subst_valid_simple assms valid.simps infer_v_wf assms
      is_satis_g_suffix wfI_suffix by metis
  moreover have "wfV Θ ℬ G v b" and "wfG Θ ℬ G" 
    using assms infer_v_wf b_of.simps apply metis  using assms infer_v_wf by metis
  ultimately show ?thesis using assms subst_valid by metis
qed

section ‹Subtyping›

lemma subst_subtype: 
  fixes v::v
  assumes "Θ ; ℬ ; Γ ⊢ v ⇒ (⦃z0:b|c0⦄)" and
    " Θ;ℬ;Γ ⊢ (⦃z0:b|c0⦄) ≲  (⦃ z : b | c ⦄)" and
    " Θ;ℬ;Γ'@((x,b,c[z::=[x]v]cv)#ΓΓ) ⊢ (⦃ z1 : b1 | c1 ⦄) ≲ (⦃ z2 : b1 | c2 ⦄)" (is " Θ ; ℬ; ?G1 ⊢ ?t1 ≲ ?t2" ) and 
    "atom z ♯ (x,v) ∧ atom z0 ♯ (c,x,v,z,Γ) ∧ atom z1 ♯ (x,v) ∧ atom z2 ♯ (x,v)" and "wsV Θ ℬ Γ v" 
  shows " Θ;ℬ;Γ'[x::=v]Γv@Γ ⊢  ⦃ z1 : b1 | c1 ⦄[x::=v]τv ≲  ⦃ z2 : b1 | c2 ⦄[x::=v]τv"
proof -
  have z2: "atom z2 ♯ (x,v) " using assms by auto
  hence "x ≠ z2" by auto

  obtain xx::x where xxf: "atom xx ♯ (x,z1, c1, z2, c2, Γ' @ (x, b, c[z::=[x]v]cv) #Γ Γ, c1[x::=v]cv, c2[x::=v]cv, Γ'[x::=v]Γv @ Γ, 
                (Θ , ℬ  , Γ'[x::=v]Γv@Γ,   z1 , c1[x::=v]cv ,  z2 ,     c2[x::=v]cv  ))" (is "atom xx ♯ ?tup")
    using obtain_fresh by blast
  hence xxf2: "atom xx ♯ (z1, c1, z2, c2, Γ' @ (x, b, c[z::=[x]v]cv) #Γ Γ)" using fresh_prod9 fresh_prod5 by fast    

  have  vd1: " Θ;ℬ;((xx, b1, c1[z1::=V_var xx]cv) #Γ Γ')[x::=v]Γv @ Γ  ⊨ (c2[z2::=V_var xx]cv)[x::=v]cv"
  proof(rule subst_valid_infer_v[of Θ _ _ _ z0 b c0 _ c, where z=z])
    show "Θ ; ℬ ; Γ  ⊢ v ⇒ ⦃ z0 : b  | c0 ⦄" using assms by auto

    show xf: "atom x ♯ Γ" using subtype_g_wf wfG_inside_fresh_suffix assms by metis

    show "atom x ♯ c" proof -
      have "wfT  Θ ℬ Γ (⦃ z : b | c ⦄)" using subtype_wf[OF assms(2)] by auto
      moreover have "x ≠ z" using assms(4) 
        using fresh_Pair not_self_fresh by blast
      ultimately show ?thesis using xf wfT_fresh_c assms by presburger
    qed

    show " Θ ; ℬ⊢wf ((xx, b1, c1[z1::=V_var xx]cv) #Γ Γ') @ (x, b, c[z::=[x]v]cv) #Γ Γ "
    proof(subst append_g.simps,rule wfG_consI)
      show *: ‹ Θ ; ℬ⊢wf Γ' @ (x, b, c[z::=[x]v]cv) #Γ Γ › using subtype_g_wf assms by metis
      show ‹atom xx ♯ Γ' @ (x, b, c[z::=[x]v]cv) #Γ Γ›  using xxf fresh_prod9 by metis
      show ‹ Θ ; ℬ⊢wf b1 › using subtype_elims[OF assms(3)] wfT_wfC wfC_wf wfG_cons by metis
      show "Θ ; ℬ ; (xx, b1, TRUE) #Γ Γ' @ (x, b, c[z::=[x]v]cv) #Γ Γ ⊢wf c1[z1::=V_var xx]cv " proof(rule  wfT_wfC)
        have "⦃ z1 : b1  | c1 ⦄ =  ⦃ xx : b1  | c1[z1::=V_var xx]cv ⦄ " using xxf fresh_prod9 type_eq_subst xxf2 fresh_prodN by metis
        thus "Θ ; ℬ ; Γ' @ (x, b, c[z::=[x]v]cv) #Γ Γ  ⊢wf ⦃ xx : b1  | c1[z1::=V_var xx]cv ⦄ " using subtype_wfT[OF assms(3)] by metis
        show "atom xx ♯ Γ' @ (x, b, c[z::=[x]v]cv) #Γ Γ" using xxf fresh_prod9 by metis
      qed       
    qed

    show "atom z0 ♯ v" using assms fresh_prod5 by auto
    have "Θ ; ℬ ; (z0, b, c0) #Γ Γ  ⊨ c[z::=V_var z0]v "     
      apply(rule obtain_fresh[of "(z0,c0, Γ, c, z)"],rule subtype_valid[OF assms(2), THEN valid_flip], 
          (fastforce simp add: assms fresh_prodN)+) done
    thus  "Θ ; ℬ ; (z0, b, c0) #Γ Γ  ⊨ c[z::=V_var z0]cv "   using subst_defs by auto

    show "atom z0 ♯ c" using assms fresh_prod5 by auto
    show "Θ ; ℬ ; ((xx, b1, c1[z1::=V_var xx]cv) #Γ Γ') @ (x, b, c[z::=[x]v]cv) #Γ Γ  ⊨ c2[z2::=V_var xx]cv "
      using subtype_valid  assms(3) xxf xxf2 fresh_prodN append_g.simps subst_defs by metis
  qed

  have xfw1: "atom z1 ♯ v ∧ atom x ♯ [ xx ]v ∧ x ≠ z1" 
    apply(intro conjI)
    apply(simp add: assms xxf fresh_at_base fresh_prodN freshers fresh_x_neq)+
    using fresh_x_neq fresh_prodN xxf  apply blast
    using fresh_x_neq fresh_prodN assms by blast

  have xfw2: "atom z2 ♯ v ∧ atom x ♯ [ xx ]v ∧ x ≠ z2"     
    apply(auto simp add: assms xxf fresh_at_base fresh_prodN freshers)
    by(insert xxf fresh_at_base fresh_prodN assms, fast+) 

  have wf1: "wfT Θ ℬ (Γ'[x::=v]Γv@Γ) (⦃ z1 : b1  | c1[x::=v]cv ⦄)" proof -
    have "wfT Θ ℬ (Γ'[x::=v]Γv@Γ) (⦃ z1 : b1  | c1 ⦄)[x::=v]τv" 
      using wf_subst(4)  assms b_of.simps infer_v_v_wf subtype_wf subst_tv.simps subst_g_inside  wfT_wf by metis
    moreover have "atom z1 ♯ (x,v)" using assms by auto
    ultimately show ?thesis using subst_tv.simps by auto
  qed
  moreover have wf2: "wfT Θ ℬ (Γ'[x::=v]Γv@Γ) (⦃ z2 : b1  | c2[x::=v]cv ⦄)" proof -
    have "wfT Θ ℬ (Γ'[x::=v]Γv@Γ) (⦃ z2 : b1  | c2 ⦄)[x::=v]τv" using wf_subst(4)  assms b_of.simps infer_v_v_wf subtype_wf subst_tv.simps subst_g_inside  wfT_wf by metis
    moreover have "atom z2 ♯ (x,v)" using assms by auto
    ultimately show ?thesis using subst_tv.simps by auto
  qed
  moreover have "Θ ; ℬ ; (xx, b1, c1[x::=v]cv[z1::=V_var xx]cv) #Γ (Γ'[x::=v]Γv @ Γ )  ⊨ (c2[x::=v]cv)[z2::=V_var xx]cv" proof -
    have "xx ≠ x" using  xxf fresh_Pair fresh_at_base by fast
    hence "((xx, b1, subst_cv c1 z1 (V_var xx) ) #Γ Γ')[x::=v]Γv = (xx, b1, (subst_cv c1 z1 (V_var xx) )[x::=v]cv) #Γ (Γ'[x::=v]Γv)"
      using subst_gv.simps by auto
    moreover have "(c1[z1::=V_var xx]cv )[x::=v]cv = (c1[x::=v]cv) [z1::=V_var xx]cv" using subst_cv_commute_full xfw1 by metis
    moreover have "c2[z2::=[ xx ]v]cv[x::=v]cv  =  (c2[x::=v]cv)[z2::=V_var xx]cv" using subst_cv_commute_full xfw2 by metis
    ultimately show ?thesis using  vd1  append_g.simps by metis
  qed
  moreover have "atom xx ♯ (Θ , ℬ  , Γ'[x::=v]Γv@Γ,  z1 , c1[x::=v]cv ,  z2  ,c2[x::=v]cv  )" 
    using xxf fresh_prodN by metis
  ultimately have  "Θ ; ℬ ; Γ'[x::=v]Γv@Γ  ⊢ ⦃ z1 : b1  | c1[x::=v]cv ⦄ ≲ ⦃ z2 : b1  | c2[x::=v]cv ⦄" 
    using subtype_baseI  subst_defs  by metis
  thus ?thesis using subst_tv.simps assms by presburger
qed

lemma subst_subtype_tau: 
  fixes v::v
  assumes   "Θ ; ℬ ; Γ ⊢ v ⇒ τ" and
    "Θ ; ℬ ; Γ ⊢ τ ≲  (⦃ z : b | c ⦄)"
    "Θ ; ℬ ; Γ'@((x,b,c[z::=[x]v]cv)#ΓΓ) ⊢ τ1 ≲ τ2" and 
    "atom z ♯ (x,v)"
  shows "Θ ; ℬ ; Γ'[x::=v]Γv@Γ ⊢  τ1[x::=v]τv     ≲  τ2[x::=v]τv"
proof - 
  obtain z0 and b0 and c0 where zbc0: "τ=(⦃ z0 : b0 | c0 ⦄) ∧ atom z0 ♯ (c,x,v,z,Γ)" 
    using obtain_fresh_z by metis
  obtain z1 and b1 and c1 where zbc1: "τ1=(⦃ z1 : b1 | c1 ⦄) ∧ atom z1 ♯ (x,v)"
    using obtain_fresh_z by metis
  obtain z2 and b2 and c2 where zbc2: "τ2=(⦃ z2 : b2 | c2 ⦄) ∧ atom z2 ♯ (x,v)"
    using obtain_fresh_z by metis

  have "b0=b" using subtype_eq_base  zbc0 assms by blast

  hence vinf: "Θ ; ℬ ; Γ ⊢ v ⇒ ⦃ z0 : b | c0 ⦄" using assms zbc0 by blast
  have vsub: "Θ ; ℬ ; Γ ⊢⦃ z0 : b | c0 ⦄ ≲  ⦃ z : b | c ⦄" using assms zbc0 ‹b0=b› by blast
  have beq:"b1=b2" using subtype_eq_base 
    using zbc1 zbc2 assms by blast 
  have "Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ ⦃ z1 : b1  | c1 ⦄[x::=v]τv ≲ ⦃ z2 : b1  | c2 ⦄[x::=v]τv" 
  proof(rule subst_subtype[OF vinf vsub] )
    show  "Θ ; ℬ ; Γ'@((x,b,c[z::=[x]v]cv)#ΓΓ) ⊢ ⦃ z1 : b1 | c1 ⦄ ≲ ⦃ z2 : b1 | c2 ⦄" 
      using beq assms zbc1 zbc2 by auto
    show "atom z ♯ (x, v) ∧ atom z0 ♯ (c, x, v, z, Γ) ∧ atom z1 ♯ (x, v) ∧ atom z2 ♯ (x, v)" 
      using zbc0 zbc1 zbc2 assms by blast
    show "wfV Θ ℬ Γ v (b_of τ)" using infer_v_wf assms by simp
  qed

  thus ?thesis using zbc1 zbc2 ‹b1=b2› assms by blast
qed

lemma subtype_if1:
  fixes v::v
  assumes "P ; ℬ ; Γ  ⊢ t1  ≲ t2" and "wfV P ℬ Γ v (base_for_lit l)" and         
    "atom z1 ♯ v" and  "atom z2 ♯ v" and "atom z1 ♯ t1" and "atom z2 ♯ t2" and "atom z1 ♯ Γ" and "atom z2 ♯ Γ"
  shows   "P ; ℬ ; Γ ⊢ ⦃ z1 : b_of t1  | CE_val v  ==  CE_val (V_lit l)   IMP  (c_of t1 z1)  ⦄ ≲ ⦃ z2 : b_of t2  | CE_val v  ==  CE_val (V_lit l) IMP  (c_of t2 z2)  ⦄"
proof - 
  obtain z1' where t1: "t1 = ⦃ z1' : b_of t1 | c_of t1 z1'⦄ ∧ atom z1' ♯ (z1,Γ,t1)" using obtain_fresh_z_c_of by metis
  obtain z2' where t2:  "t2 = ⦃ z2' : b_of t2 | c_of t2 z2'⦄ ∧ atom z2' ♯ (z2,t2) " using obtain_fresh_z_c_of by metis
  have beq:"b_of t1 = b_of t2" using subtype_eq_base2 assms by auto

  have c1: "(c_of t1 z1')[z1'::=[ z1 ]v]cv = c_of t1 z1" using c_of_switch t1 assms by simp
  have c2: "(c_of t2 z2')[z2'::=[ z2 ]v]cv = c_of t2 z2" using c_of_switch t2 assms by simp

  have "P ; ℬ ; Γ  ⊢ ⦃ z1 : b_of t1  | [ v ]ce  ==  [ [ l ]v ]ce   IMP  (c_of t1 z1')[z1'::=[z1]v]v  ⦄ ≲ ⦃ z2 : b_of t1  | [ v ]ce  ==  [ [ l ]v ]ce   IMP  (c_of t2 z2')[z2'::=[z2]v]v  ⦄"
  proof(rule subtype_if)
    show ‹P ; ℬ ; Γ  ⊢ ⦃ z1' : b_of t1  | c_of t1 z1' ⦄ ≲ ⦃ z2' : b_of t1  | c_of t2 z2' ⦄› using t1 t2 assms beq by auto
    show ‹ P ; ℬ ; Γ  ⊢wf ⦃ z1 : b_of t1  | [ v ]ce  ==  [ [ l ]v ]ce   IMP  (c_of t1 z1')[z1'::=[ z1 ]v]v  ⦄ › using wfT_wfT_if_rev assms subtype_wfT c1 subst_defs by metis
    show ‹ P ; ℬ ; Γ  ⊢wf ⦃ z2 : b_of t1  | [ v ]ce  ==  [ [ l ]v ]ce   IMP  (c_of t2 z2')[z2'::=[ z2 ]v]v  ⦄ › using wfT_wfT_if_rev assms subtype_wfT c2 subst_defs beq by metis
    show ‹atom z1 ♯ v› using assms by auto
    show ‹atom z1' ♯ Γ› using t1 by auto
    show ‹atom z1 ♯ c_of t1 z1'› using t1 assms c_of_fresh by force
    show ‹atom z2 ♯ c_of t2 z2'› using t2 assms c_of_fresh by force
    show ‹atom z2 ♯ v› using assms by auto
  qed
  then show ?thesis using t1 t2 assms c1 c2 beq subst_defs by metis
qed

section ‹Values›

lemma subst_infer_aux:
  fixes τ1::τ and v'::v
  assumes "Θ ; ℬ ; Γ ⊢ v'[x::=v]vv ⇒ τ1" and "Θ ; ℬ ; Γ' ⊢ v' ⇒ τ2" and "b_of τ1 = b_of τ2"
  shows "τ1 = (τ2[x::=v]τv)"
proof -
  obtain z1 and b1 where zb1: "τ1 = (⦃ z1 : b1 | C_eq (CE_val (V_var z1)) (CE_val (v'[x::=v]vv)) ⦄) ∧ atom z1 ♯ ((CE_val (v'[x::=v]vv), CE_val v),v'[x::=v]vv)" 
    using infer_v_form_fresh[OF assms(1)] by fastforce
  obtain z2 and b2 where zb2: "τ2 = (⦃ z2 : b2 | C_eq (CE_val (V_var z2)) (CE_val v') ⦄) ∧ atom z2 ♯ ((CE_val (v'[x::=v]vv), CE_val v,x,v),v')" 
    using infer_v_form_fresh [OF assms(2)] by fastforce
  have beq: "b1 = b2" using assms zb1 zb2 by simp

  hence "(⦃ z2 : b2 | C_eq (CE_val (V_var z2)) (CE_val v') ⦄)[x::=v]τv = (⦃ z2 : b2 | C_eq (CE_val (V_var z2)) (CE_val (v'[x::=v]vv)) ⦄)" 
    using subst_tv.simps subst_cv.simps subst_ev.simps  forget_subst_vv[of x "V_var z2"] zb2 by force 
  also have  "... = (⦃ z1 : b1 | C_eq (CE_val (V_var z1)) (CE_val (v'[x::=v]vv)) ⦄)" 
    using type_e_eq[of z2 "CE_val  (v'[x::=v]vv)"z1 b1 ] zb1 zb2 fresh_PairD(1) assms beq by metis
  finally show ?thesis using zb1  zb2 by argo
qed

lemma subst_t_b_eq:
  fixes x::x and v::v
  shows  "b_of (τ[x::=v]τv) = b_of τ"
proof - 
  obtain z and b and c where "τ = ⦃ z : b | c ⦄ ∧ atom z ♯ (x,v)"
    using has_fresh_z by blast
  thus ?thesis using subst_tv.simps  by simp
qed

lemma fresh_g_fresh_v:
  fixes x::x
  assumes "atom x ♯ Γ" and "wfV Θ ℬ Γ v b"
  shows "atom x ♯ v"
  using assms  wfV_supp wfX_wfY wfG_atoms_supp_eq fresh_def 
  by (metis wfV_x_fresh)

lemma infer_v_fresh_g_fresh_v:
  fixes x::x and Γ::Γ and v::v
  assumes "atom x ♯ Γ'@Γ" and "Θ ; ℬ ; Γ ⊢ v ⇒ τ" 
  shows "atom x ♯ v"
proof - 
  have "atom x ♯ Γ" using fresh_suffix assms by auto
  moreover have "wfV Θ ℬ Γ v (b_of τ)" using infer_v_wf assms by auto
  ultimately show ?thesis using fresh_g_fresh_v by metis
qed

lemma infer_v_fresh_g_fresh_xv:
  fixes xa::x and v::v and Γ::Γ
  assumes "atom xa ♯ Γ'@((x,b,c[z::=[x]v]cv)#ΓΓ)" and "Θ ; ℬ ; Γ ⊢ v ⇒ τ" 
  shows "atom xa ♯ (x,v)"
proof -
  have "atom xa ♯ x" using assms  fresh_in_g fresh_def by blast
  moreover have "Γ'@((x,b,c[z::=[x]v]cv)#ΓΓ) = ((Γ'@(x,b,c[z::=[x]v]cv)#ΓGNil)@Γ)" using append_g.simps append_g_assoc by simp
  moreover hence "atom xa ♯ v" using infer_v_fresh_g_fresh_v assms by metis
  ultimately show ?thesis by auto
qed

lemma wfG_subst_infer_v:
  fixes v::v
  assumes "Θ ; ℬ ⊢wf Γ' @ (x, b, c0[z0::=[x]v]cv) #Γ Γ" and "Θ ; ℬ ; Γ ⊢ v ⇒ τ" and "b_of τ = b"
  shows "Θ ; ℬ⊢wf Γ'[x::=v]Γv @ Γ "
  using wfG_subst_wfV infer_v_v_wf assms by auto

lemma fresh_subst_gv_inside:
  fixes Γ::Γ
  assumes "atom z ♯ Γ' @ (x, b1, c0[z0::=[ x ]v]cv) #Γ Γ" and "atom z ♯ v" 
  shows "atom z ♯ Γ'[x::=v]Γv@Γ" 
  unfolding fresh_append_g  using fresh_append_g assms fresh_subst_gv fresh_GCons by metis

lemma subst_t:
  fixes x::x and b::b and xa::x
  assumes "atom z ♯ x" and "atom z ♯ v"
  shows   "(⦃ z : b  | [ [ z ]v ]ce  ==  [ v'[x::=v]vv ]ce  ⦄) = (⦃ z : b  | [ [ z ]v ]ce  ==  [ v']ce  ⦄[x::=v]τv)"
  using assms subst_vv.simps subst_tv.simps subst_cv.simps subst_cev.simps by auto

lemma infer_l_fresh:
  assumes  "⊢ l ⇒ τ"
  shows "atom x ♯ τ"
proof -
  have "[] ; {||}  ⊢wf GNil" using wfG_nilI wfTh_emptyI by auto
  hence "[] ; {||} ; GNil   ⊢wf τ" using assms infer_l_wf by auto
  thus ?thesis using  fresh_def wfT_supp by force
qed

lemma subst_infer_v:
  fixes v::v and v'::v
  assumes "Θ ; ℬ ;  Γ'@((x,b1,c0[z0::=[x]v]cv)#ΓΓ) ⊢ v' ⇒ τ2" and 
    "Θ ; ℬ ; Γ ⊢ v ⇒ τ1" and           
    "Θ ; ℬ ; Γ ⊢ τ1 ≲  (⦃ z0 : b1 | c0 ⦄)" and "atom z0 ♯ (x,v)"
  shows "Θ ; ℬ ; (Γ'[x::=v]Γv)@Γ  ⊢ v'[x::=v]vv  ⇒ τ2[x::=v]τv"
  using assms proof(nominal_induct "Γ'@((x,b1,c0[z0::=[x]v]cv)#ΓΓ)" v' τ2 avoiding: x v   rule: infer_v.strong_induct)
  case (infer_v_varI Θ ℬ b c xa z)
  have "Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ [ xa ]v[x::=v]vv ⇒ ⦃ z : b  | [ [ z ]v ]ce  ==  [ [ xa ]v[x::=v]vv ]ce  ⦄" 
  proof(cases "x=xa")
    case True   
    have  "Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ v ⇒ ⦃ z : b  | [ [ z ]v ]ce  ==  [ v ]ce  ⦄" 
    proof(rule infer_v_g_weakening)
      show *:‹ Θ ; ℬ ; Γ ⊢ v ⇒ ⦃ z : b  | [ [ z ]v ]ce  ==  [ v ]ce  ⦄› 
        using infer_v_form infer_v_varI 
        by (metis True lookup_inside_unique_b lookup_inside_wf ms_fresh_all(32) subtype_eq_base type_e_eq)
      show ‹toSet Γ ⊆ toSet (Γ'[x::=v]Γv @ Γ)› by simp
      have "Θ ; ℬ ; Γ ⊢wf v : b1" using infer_v_wf subtype_eq_base2 b_of.simps infer_v_varI by metis
      thus  ‹ Θ ; ℬ  ⊢wf Γ'[x::=v]Γv @ Γ › 
        using wfG_subst[OF infer_v_varI(3), of Γ' x b1 "c0[z0::=[ x ]v]cv" Γ v] subst_g_inside infer_v_varI by metis
    qed

    thus ?thesis using subst_vv.simps True by simp
  next
    case False
    then obtain c' where c: "Some (b, c') = lookup (Γ'[x::=v]Γv @ Γ) xa" using lookup_subst2 infer_v_varI by metis
    have "Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ [ xa ]v ⇒ ⦃ z : b  | [ [ z ]v ]ce  ==  [ [ xa ]v ]ce  ⦄" 
    proof
      have "Θ ; ℬ ; Γ ⊢wf v : b1" using infer_v_wf subtype_eq_base2 b_of.simps infer_v_varI by metis
      thus "Θ ; ℬ  ⊢wf Γ'[x::=v]Γv @ Γ" using infer_v_varI
        using wfG_subst[OF infer_v_varI(3), of Γ' x b1 "c0[z0::=[ x ]v]cv" Γ v] subst_g_inside infer_v_varI by metis
      show "atom z ♯ xa" using infer_v_varI by auto
      show "Some (b, c') = lookup (Γ'[x::=v]Γv @ Γ) xa" using c  by auto
      show "atom z ♯ (Θ, ℬ, Γ'[x::=v]Γv @ Γ)" by (fresh_mth add: infer_v_varI fresh_subst_gv_inside)
    qed    
    then show ?thesis using subst_vv.simps False by simp
  qed 
  thus ?case using subst_t fresh_prodN infer_v_varI by metis
next
  case (infer_v_litI Θ ℬ l τ)
  show ?case unfolding subst_vv.simps proof
    show "Θ ; ℬ  ⊢wf Γ'[x::=v]Γv @ Γ" using wfG_subst_infer_v infer_v_litI subtype_eq_base2 b_of.simps by metis
    have "atom x ♯ τ" using infer_v_litI infer_l_fresh by metis
    thus  "⊢ l ⇒ τ[x::=v]τv" using infer_v_litI type_v_subst_fresh by simp
  qed
next
  case (infer_v_pairI z v1 v2 Θ ℬ t1 t2)
  have " Θ ; ℬ ; Γ'[x::=v]Γv @
              Γ ⊢ [ v1[x::=v]vv , v2[x::=v]vv ]v ⇒ ⦃ z : [ b_of t1[x::=v]τv , b_of
      t2[x::=v]τv ]b  | [ [ z ]v ]ce  ==  [ [ v1[x::=v]vv , v2[x::=v]vv ]v ]ce  ⦄" 
  proof
    show ‹atom z ♯ (v1[x::=v]vv, v2[x::=v]vv)› by (fresh_mth add: infer_v_pairI)
    show ‹atom z ♯ (Θ, ℬ, Γ'[x::=v]Γv @ Γ)›  by (fresh_mth add: infer_v_pairI fresh_subst_gv_inside)
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ v1[x::=v]vv ⇒ t1[x::=v]τv› using infer_v_pairI by metis
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ v2[x::=v]vv ⇒ t2[x::=v]τv› using infer_v_pairI by metis
  qed
  then show ?case using  subst_vv.simps subst_tv.simps infer_v_pairI b_of_subst by simp
next
  case (infer_v_consI s dclist Θ dc tc ℬ va tv z)

  have " Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ (V_cons s dc va[x::=v]vv) ⇒ ⦃ z : B_id s  | [ [ z ]v ]ce  ==  [ V_cons s dc va[x::=v]vv ]ce  ⦄" 
  proof
    show td:‹AF_typedef s dclist ∈ set Θ› using infer_v_consI by auto
    show dc:‹(dc, tc) ∈ set dclist› using infer_v_consI by auto
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ va[x::=v]vv ⇒ tv[x::=v]τv› using infer_v_consI by auto
    have ‹Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ tv[x::=v]τv ≲ tc[x::=v]τv› 
      using    subst_subtype_tau infer_v_consI by metis
    moreover have "atom x ♯ tc" using wfTh_lookup_supp_empty[OF td dc] infer_v_wf infer_v_consI fresh_def by fast
    ultimately show ‹Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ tv[x::=v]τv ≲ tc› by simp 
    show ‹atom z ♯ va[x::=v]vv› using infer_v_consI by auto
    show ‹atom z ♯ (Θ, ℬ, Γ'[x::=v]Γv @ Γ)› by (fresh_mth add: infer_v_consI fresh_subst_gv_inside)
  qed  
  thus ?case using subst_vv.simps subst_t[of z x v ] infer_v_consI by metis

next
  case (infer_v_conspI s bv dclist Θ dc tc ℬ va tv b z)
  have "Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ (V_consp s dc b va[x::=v]vv) ⇒ ⦃ z : B_app s b  | [ [ z ]v ]ce  ==  [ V_consp s dc b va[x::=v]vv ]ce  ⦄"
  proof
    show td:‹AF_typedef_poly s bv dclist ∈ set Θ› using infer_v_conspI by auto
    show dc:‹(dc, tc) ∈ set dclist› using infer_v_conspI by auto
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ va[x::=v]vv ⇒ tv[x::=v]τv› using  infer_v_conspI by metis
    have ‹Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ tv[x::=v]τv ≲ tc[bv::=b]τb[x::=v]τv› 
      using    subst_subtype_tau infer_v_conspI by metis
    moreover  have "atom x ♯ tc[bv::=b]τb" proof -
      have "supp tc ⊆ { atom bv }" using wfTh_poly_lookup_supp infer_v_conspI wfX_wfY by metis
      hence "atom x ♯ tc" using x_not_in_b_set 
        using fresh_def by fastforce
      moreover have "atom x ♯ b" using x_fresh_b by auto
      ultimately show ?thesis using fresh_subst_if subst_b_τ_def by metis
    qed
    ultimately show ‹Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ tv[x::=v]τv ≲ tc[bv::=b]τb› by simp 
    show ‹atom z ♯ (Θ, ℬ, Γ'[x::=v]Γv @ Γ, va[x::=v]vv, b)›  proof -
      have "atom z ♯ va[x::=v]vv" using fresh_subst_v_if infer_v_conspI subst_v_v_def by metis
      moreover have "atom z ♯ Γ'[x::=v]Γv @ Γ"  using fresh_subst_gv_inside infer_v_conspI by metis
      ultimately show ?thesis using fresh_prodN infer_v_conspI by metis
    qed
    show ‹atom bv ♯ (Θ, ℬ, Γ'[x::=v]Γv @ Γ, va[x::=v]vv, b)›  proof -
      have "atom bv ♯ va[x::=v]vv" using fresh_subst_v_if infer_v_conspI subst_v_v_def by metis
      moreover have "atom bv ♯ Γ'[x::=v]Γv @ Γ"  using fresh_subst_gv_inside infer_v_conspI by metis
      ultimately show ?thesis using fresh_prodN infer_v_conspI by metis
    qed
    show  "Θ ; ℬ  ⊢wf b" using infer_v_conspI by auto
  qed
  thus ?case using subst_vv.simps  subst_t[of z x v ] infer_v_conspI by metis

qed

lemma subst_infer_check_v:
  fixes v::v and v'::v
  assumes "Θ ; ℬ ; Γ ⊢ v ⇒ τ1"  and
    "check_v Θ ℬ (Γ'@((x,b1,c0[z0::=[x]v]cv)#ΓΓ))  v' τ2"  and
    "Θ ; ℬ ; Γ ⊢ τ1 ≲  ⦃ z0 : b1 | c0 ⦄" and "atom z0 ♯ (x,v)"
  shows "check_v Θ ℬ ((Γ'[x::=v]Γv)@Γ)  (v'[x::=v]vv) (τ2[x::=v]τv)"
proof -
  obtain τ2' where t2: "infer_v  Θ ℬ  (Γ' @ (x, b1, c0[z0::=[x]v]cv) #Γ Γ)  v' τ2' ∧  Θ ; ℬ ; (Γ' @ (x, b1, c0[z0::=[x]v]cv) #Γ Γ)  ⊢ τ2' ≲ τ2"
    using check_v_elims assms by blast
  hence "infer_v Θ ℬ ((Γ'[x::=v]Γv)@Γ)  (v'[x::=v]vv)  (τ2'[x::=v]τv)"
    using subst_infer_v[OF _ assms(1)  assms(3) assms(4)] by blast
  moreover hence "Θ;  ℬ ; ((Γ'[x::=v]Γv)@Γ) ⊢τ2'[x::=v]τv ≲  τ2[x::=v]τv" 
    using subst_subtype assms t2 by (meson subst_subtype_tau subtype_trans)
  ultimately show ?thesis using check_v.intros by blast
qed

lemma type_veq_subst[simp]:
  assumes "atom z ♯ (x,v)"
  shows "⦃ z : b | CE_val (V_var z)  ==  CE_val v'  ⦄[x::=v]τv = ⦃ z : b | CE_val (V_var z)  ==  CE_val v'[x::=v]vv  ⦄"
  using assms by auto

lemma subst_infer_v_form:
  fixes v::v and v'::v and Γ::Γ
  assumes  "Θ ; ℬ ; Γ ⊢ v ⇒ τ1" and 
    "Θ ; ℬ ; Γ'@((x,b1,c0[z0::=[x]v]cv)#ΓΓ) ⊢ v' ⇒ τ2" and "b= b_of τ2"
    "Θ ; ℬ ; Γ ⊢ τ1 ≲  (⦃ z0 : b1 | c0 ⦄)" and "atom z0 ♯ (x,v)" and "atom z3' ♯ (x,v,v', Γ'@((x,b1,c0[z0::=[x]v]cv)#ΓΓ) )"
  shows ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇒ ⦃ z3' : b | CE_val (V_var z3')  ==  CE_val v'[x::=v]vv  ⦄›
proof - 
  have "Θ ; ℬ ; Γ'@((x,b1,c0[z0::=[x]v]cv)#ΓΓ) ⊢ v' ⇒ ⦃ z3' : b_of τ2 |  C_eq (CE_val (V_var z3')) (CE_val v') ⦄" 
  proof(rule infer_v_form4)
    show ‹ Θ ; ℬ ; Γ' @ (x, b1, c0[z0::=[ x ]v]cv) #Γ Γ ⊢ v' ⇒ τ2› using assms by metis
    show ‹atom z3' ♯ (v', Γ' @ (x, b1, c0[z0::=[ x ]v]cv) #Γ Γ)› using assms fresh_prodN by metis
    show ‹b_of τ2 = b_of τ2› by auto
  qed
  hence ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇒ ⦃ z3' : b_of τ2 | CE_val (V_var z3')  ==  CE_val v'  ⦄[x::=v]τv› 
    using subst_infer_v assms by metis
  thus ?thesis using type_veq_subst fresh_prodN assms by metis
qed

section ‹Expressions›

text ‹
    For operator, fst and snd cases, we use elimination to get one or more values, apply the substitution lemma for values. The types always have
the same form and are equal under substitution.
    For function application, the subst value is a subtype of the value which is a subtype of the argument. The return of the function is the same
    under substitution.
›

text ‹ Observe a similar pattern for each case ›

lemma subst_infer_e:
  fixes v::v and e::e and Γ'::Γ
  assumes 
    "Θ ; Φ ; ℬ ; G ; Δ ⊢ e ⇒ τ2" and "G = (Γ'@((x,b1,subst_cv c0 z0 (V_var x))#ΓΓ))"
    "Θ ; ℬ ; Γ ⊢ v ⇒ τ1" and 
    "Θ;  ℬ ; Γ ⊢ τ1 ≲  ⦃ z0 : b1 | c0 ⦄" and "atom z0 ♯ (x,v)"
  shows "Θ ; Φ ; ℬ ; ((Γ'[x::=v]Γv)@Γ) ; (Δ[x::=v]Δv)  ⊢ (subst_ev e x v )  ⇒ τ2[x::=v]τv"
  using assms proof(nominal_induct  avoiding: x v rule: infer_e.strong_induct)
  case (infer_e_valI Θ ℬ Γ'' Δ Φ v' τ)

  have "Θ ; Φ ; ℬ ; Γ'[x::=v]Γv @ Γ ;  Δ[x::=v]Δv   ⊢ (AE_val (v'[x::=v]vv)) ⇒ τ[x::=v]τv"  
  proof
    show "Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv"  using wfD_subst infer_e_valI subtype_eq_base2 
      by (metis b_of.simps infer_v_v_wf subst_g_inside_simple wfD_wf wf_subst(11))
    show "Θ⊢wf Φ" using infer_e_valI by auto
    show "Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇒ τ[x::=v]τv" using subst_infer_v infer_e_valI using wfD_subst infer_e_valI subtype_eq_base2 
      by metis
  qed       
  thus ?case using subst_ev.simps by simp
next
  case (infer_e_plusI Θ ℬ Γ'' Δ Φ v1 z1 c1 v2 z2 c2 z3)

  hence z3f: "atom z3 ♯ CE_op Plus [v1]ce [v2]ce" using e.fresh ce.fresh opp.fresh by metis

  obtain z3'::x where *:"atom z3' ♯ (x,v,AE_op Plus v1 v2,   CE_op Plus [v1]ce [v2]ce , AE_op Plus v1[x::=v]vv v2[x::=v]vv , CE_op Plus [v1[x::=v]vv]ce [v2[x::=v]vv]ce,Γ'[x::=v]Γv @ Γ )" 
    using obtain_fresh by metis
  hence  **:"(⦃ z3 : B_int  | CE_val (V_var z3)  ==  CE_op Plus [v1]ce [v2]ce  ⦄) = ⦃ z3' : B_int  | CE_val (V_var z3')  ==  CE_op Plus [v1]ce [v2]ce  ⦄" 
    using type_e_eq  infer_e_plusI fresh_Pair z3f by metis

  obtain z1' b1' c1' where  z1:"atom z1' ♯ (x,v) ∧ ⦃ z1 : B_int | c1 ⦄ = ⦃ z1' : b1' | c1' ⦄" using obtain_fresh_z by metis
  obtain z2' b2'  c2' where z2:"atom z2' ♯ (x,v) ∧ ⦃ z2 : B_int | c2 ⦄ = ⦃ z2' : b2' | c2' ⦄" using obtain_fresh_z by metis

  have bb:"b1' = B_int ∧ b2' = B_int" using z1 z2 τ.eq_iff by metis

  have "Θ ; Φ ; ℬ ; Γ'[x::=v]Γv @ Γ ; Δ[x::=v]Δv  ⊢ (AE_op Plus (v1[x::=v]vv) (v2[x::=v]vv)) ⇒ ⦃ z3' : B_int  | CE_val (V_var z3')  ==  CE_op Plus ([v1[x::=v]vv]ce) ([v2[x::=v]vv]ce)  ⦄"
  proof 
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv › 
      using infer_e_plusI wfD_subst subtype_eq_base2 b_of.simps by metis
    show ‹ Θ⊢wf Φ › using  infer_e_plusI by blast
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v1[x::=v]vv ⇒ ⦃ z1' : B_int  | c1'[x::=v]cv ⦄› using subst_tv.simps subst_infer_v infer_e_plusI z1 bb by metis
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v2[x::=v]vv ⇒ ⦃ z2' : B_int  | c2'[x::=v]cv ⦄› using subst_tv.simps subst_infer_v infer_e_plusI z2 bb by metis
    show ‹atom z3' ♯ AE_op Plus v1[x::=v]vv v2[x::=v]vv› using fresh_prod6 * by metis
    show ‹atom z3' ♯ Γ'[x::=v]Γv @ Γ› using * by auto
  qed
  moreover have "⦃ z3' : B_int  | CE_val (V_var z3')  ==  CE_op Plus ([v1[x::=v]vv]ce) ([v2[x::=v]vv]ce)  ⦄ = ⦃ z3' : B_int  | CE_val (V_var z3')  ==  CE_op Plus [v1]ce [v2]ce  ⦄[x::=v]τv"
    by(subst subst_tv.simps,auto simp add: * )
  ultimately show ?case using subst_ev.simps * ** by metis
next
  case (infer_e_leqI Θ ℬ Γ'' Δ Φ v1 z1 c1 v2 z2 c2 z3)

  hence z3f: "atom z3 ♯ CE_op LEq [v1]ce [v2]ce" using e.fresh ce.fresh opp.fresh by metis

  obtain z3'::x where *:"atom z3' ♯ (x,v,AE_op LEq v1 v2, CE_op LEq [v1]ce [v2]ce , CE_op LEq [v1[x::=v]vv]ce [v2[x::=v]vv]ce , AE_op LEq v1[x::=v]vv v2[x::=v]vv,Γ'[x::=v]Γv @ Γ )"  
    using obtain_fresh by metis
  hence  **:"(⦃ z3 : B_bool  | CE_val (V_var z3)  ==  CE_op LEq [v1]ce [v2]ce  ⦄) = ⦃ z3' : B_bool  | CE_val (V_var z3')  ==  CE_op LEq [v1]ce [v2]ce  ⦄" 
    using type_e_eq  infer_e_leqI fresh_Pair z3f by metis

  obtain z1' b1' c1' where  z1:"atom z1' ♯ (x,v) ∧ ⦃ z1 : B_int | c1 ⦄ = ⦃ z1' : b1' | c1' ⦄" using obtain_fresh_z by metis
  obtain z2' b2'  c2' where z2:"atom z2' ♯ (x,v) ∧ ⦃ z2 : B_int | c2 ⦄ = ⦃ z2' : b2' | c2' ⦄" using obtain_fresh_z by metis

  have bb:"b1' = B_int ∧ b2' = B_int" using z1 z2 τ.eq_iff by metis

  have "Θ ; Φ ; ℬ ; Γ'[x::=v]Γv @ Γ ; Δ[x::=v]Δv  ⊢ (AE_op LEq (v1[x::=v]vv) (v2[x::=v]vv)) ⇒ ⦃ z3' : B_bool  | CE_val (V_var z3')  ==  CE_op LEq ([v1[x::=v]vv]ce) ([v2[x::=v]vv]ce)  ⦄"
  proof 
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv › using wfD_subst infer_e_leqI subtype_eq_base2 b_of.simps by metis
    show ‹ Θ⊢wf Φ › using  infer_e_leqI(2) by auto 
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v1[x::=v]vv ⇒ ⦃ z1' : B_int  | c1'[x::=v]cv ⦄› using subst_tv.simps subst_infer_v infer_e_leqI z1 bb by metis
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v2[x::=v]vv ⇒ ⦃ z2' : B_int  | c2'[x::=v]cv ⦄› using subst_tv.simps subst_infer_v infer_e_leqI z2 bb by metis
    show ‹atom z3' ♯ AE_op LEq v1[x::=v]vv v2[x::=v]vv› using fresh_Pair * by metis
    show ‹atom z3' ♯ Γ'[x::=v]Γv @ Γ› using * by auto
  qed
  moreover have "⦃ z3' : B_bool  | CE_val (V_var z3')  ==  CE_op LEq ([v1[x::=v]vv]ce) ([v2[x::=v]vv]ce)  ⦄ = ⦃ z3' : B_bool  | CE_val (V_var z3')  ==  CE_op LEq [v1]ce [v2]ce  ⦄[x::=v]τv"
    using subst_tv.simps subst_ev.simps * by auto
  ultimately show ?case using subst_ev.simps * ** by metis
next
  case (infer_e_eqI Θ ℬ Γ'' Δ Φ v1 z1 bb c1 v2 z2 c2 z3)

  hence z3f: "atom z3 ♯ CE_op Eq [v1]ce [v2]ce" using e.fresh ce.fresh opp.fresh by metis

  obtain z3'::x where *:"atom z3' ♯ (x,v,AE_op Eq v1 v2, CE_op Eq [v1]ce [v2]ce , CE_op Eq [v1[x::=v]vv]ce [v2[x::=v]vv]ce , AE_op Eq v1[x::=v]vv v2[x::=v]vv,Γ'[x::=v]Γv @ Γ )"  
    using obtain_fresh by metis
  hence  **:"(⦃ z3 : B_bool  | CE_val (V_var z3)  ==  CE_op Eq [v1]ce [v2]ce  ⦄) = ⦃ z3' : B_bool  | CE_val (V_var z3')  ==  CE_op Eq [v1]ce [v2]ce  ⦄" 
    using type_e_eq  infer_e_eqI fresh_Pair z3f by metis

  obtain z1' b1' c1' where  z1:"atom z1' ♯ (x,v) ∧ ⦃ z1 : bb | c1 ⦄ = ⦃ z1' : b1' | c1' ⦄" using obtain_fresh_z by metis
  obtain z2' b2'  c2' where z2:"atom z2' ♯ (x,v) ∧ ⦃ z2 : bb | c2 ⦄ = ⦃ z2' : b2' | c2' ⦄" using obtain_fresh_z by metis

  have bb:"b1' = bb ∧ b2' = bb" using z1 z2 τ.eq_iff by metis

  have "Θ ; Φ ; ℬ ; Γ'[x::=v]Γv @ Γ ; Δ[x::=v]Δv  ⊢ (AE_op Eq (v1[x::=v]vv) (v2[x::=v]vv)) ⇒ ⦃ z3' : B_bool  | CE_val (V_var z3')  ==  CE_op Eq ([v1[x::=v]vv]ce) ([v2[x::=v]vv]ce)  ⦄"
  proof 
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv › using wfD_subst infer_e_eqI subtype_eq_base2 b_of.simps by metis
    show ‹ Θ⊢wf Φ › using  infer_e_eqI(2) by auto 
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v1[x::=v]vv ⇒ ⦃ z1' : bb  | c1'[x::=v]cv ⦄› using subst_tv.simps subst_infer_v infer_e_eqI z1 bb by metis
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v2[x::=v]vv ⇒ ⦃ z2' : bb  | c2'[x::=v]cv ⦄› using subst_tv.simps subst_infer_v infer_e_eqI z2 bb by metis
    show ‹atom z3' ♯ AE_op Eq v1[x::=v]vv v2[x::=v]vv› using fresh_Pair * by metis
    show ‹atom z3' ♯ Γ'[x::=v]Γv @ Γ› using * by auto
    show "bb ∈ {B_bool, B_int, B_unit}" using infer_e_eqI by auto
  qed
  moreover have "⦃ z3' : B_bool  | CE_val (V_var z3')  ==  CE_op Eq ([v1[x::=v]vv]ce) ([v2[x::=v]vv]ce)  ⦄ = ⦃ z3' : B_bool  | CE_val (V_var z3')  ==  CE_op Eq [v1]ce [v2]ce  ⦄[x::=v]τv"
    using subst_tv.simps subst_ev.simps * by auto
  ultimately show ?case using subst_ev.simps * ** by metis
next
  case (infer_e_appI Θ ℬ Γ'' Δ Φ f x' b c τ' s' v' τ)

  hence "x ≠ x'" using ‹atom x' ♯ Γ''› using wfG_inside_x_neq wfX_wfY by metis

  show ?case proof(subst subst_ev.simps,rule)
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv › using infer_e_appI wfD_subst subtype_eq_base2 b_of.simps by metis
    show ‹ Θ⊢wf Φ ›  using  infer_e_appI by metis
    show ‹Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x' b c τ' s'))) = lookup_fun Φ f› using  infer_e_appI by metis

    have ‹Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇐ ⦃ x' : b  | c ⦄[x::=v]τv› proof(rule subst_infer_check_v )
      show "Θ ; ℬ ; Γ  ⊢ v ⇒ τ1" using infer_e_appI by metis
      show "Θ ; ℬ ; Γ' @ (x, b1, c0[z0::=[x]v]cv) #Γ Γ  ⊢ v' ⇐ ⦃ x' : b  | c ⦄" using infer_e_appI by metis
      show "Θ ; ℬ ; Γ  ⊢ τ1 ≲ ⦃ z0 : b1  | c0 ⦄" using infer_e_appI by metis
      show "atom z0 ♯ (x, v)" using infer_e_appI by metis
    qed
    moreover have "atom x ♯ c" using wfPhi_f_simple_supp_c  infer_e_appI fresh_def ‹x≠x'› 
        atom_eq_iff empty_iff infer_e_appI.hyps insert_iff subset_singletonD by metis

    moreover hence "atom x ♯ ⦃ x' : b  | c ⦄" using τ.fresh supp_b_empty fresh_def by blast
    ultimately show  ‹Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇐ ⦃ x' : b  | c ⦄› using forget_subst_tv by metis

    have *: "atom x' ♯ (x,v)" using infer_v_fresh_g_fresh_xv infer_e_appI check_v_wf by blast

    show  ‹atom x' ♯ (Θ, Φ, ℬ, Γ'[x::=v]Γv @ Γ, Δ[x::=v]Δv, v'[x::=v]vv, τ[x::=v]τv)›   
      apply(unfold fresh_prodN, intro conjI)
      apply (fresh_subst_mth_aux add:  infer_e_appI fresh_subst_gv  wfD_wf subst_g_inside)
      using infer_e_appI fresh_subst_gv  wfD_wf subst_g_inside apply metis
      using infer_e_appI      fresh_subst_dv_if apply metis
      done

    have "supp τ' ⊆ { atom x' } ∪ supp ℬ" using infer_e_appI wfT_supp wfPhi_f_simple_wfT 
      by (meson infer_e_appI.hyps(2) le_supI1 wfPhi_f_simple_supp_t)
    hence "atom x ♯ τ'" using  ‹x≠x'› fresh_def supp_at_base x_not_in_b_set  by fastforce
    thus  ‹τ'[x'::=v'[x::=v]vv]v = τ[x::=v]τv› using subst_tv_commute infer_e_appI subst_defs by metis
  qed
next
  case (infer_e_appPI Θ ℬ Γ'' Δ Φ b' f bv x' b c τ' s' v' τ)

  hence "x ≠ x'" using ‹atom x' ♯ Γ''› using wfG_inside_x_neq wfX_wfY by metis

  show ?case proof(subst subst_ev.simps,rule)
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv ›  using infer_e_appPI wfD_subst subtype_eq_base2 b_of.simps by metis
    show ‹ Θ⊢wf Φ ›  using  infer_e_appPI(4) by auto
    show "Θ ; ℬ ⊢wf b'"  using  infer_e_appPI(5) by auto
    show "Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x' b c τ' s'))) = lookup_fun Φ f"  using  infer_e_appPI(6) by auto

    show "Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇐ ⦃ x' : b[bv::=b']b  | c[bv::=b']b ⦄" proof -
      have ‹Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇐ ⦃ x' : b[bv::=b']bb  | c[bv::=b']cb ⦄[x::=v]τv› proof(rule subst_infer_check_v )
        show "Θ ; ℬ ; Γ  ⊢ v ⇒ τ1" using infer_e_appPI by metis
        show "Θ ; ℬ ; Γ' @ (x, b1, c0[z0::=[x]v]cv) #Γ Γ  ⊢ v' ⇐ ⦃ x' : b[bv::=b']bb  | c[bv::=b']cb ⦄" using infer_e_appPI subst_defs by metis
        show "Θ ; ℬ ; Γ  ⊢ τ1 ≲ ⦃ z0 : b1  | c0 ⦄" using infer_e_appPI by metis
        show "atom z0 ♯ (x, v)" using infer_e_appPI by metis
      qed
      moreover have "atom x ♯ c"  proof -
        have "supp c ⊆ {atom x', atom bv}" using  wfPhi_f_poly_supp_c[OF infer_e_appPI(6)] infer_e_appPI by metis
        thus ?thesis unfolding fresh_def using  ‹x≠x'›  atom_eq_iff by auto
      qed
      moreover hence "atom x ♯ ⦃ x' : b[bv::=b']bb  | c[bv::=b']cb ⦄" using τ.fresh supp_b_empty fresh_def subst_b_fresh_x 
        by (metis subst_b_c_def)
      ultimately show ?thesis using forget_subst_tv subst_defs by metis
    qed
    have "supp τ' ⊆ { atom x', atom bv }" using  wfPhi_f_poly_supp_t infer_e_appPI by metis
    hence "atom x ♯ τ'" using fresh_def ‹x≠x'› by force
    hence *:"atom x ♯ τ'[bv::=b']τb" using    subst_b_fresh_x subst_b_τ_def by metis
    have "atom x' ♯ (x,v)" using infer_v_fresh_g_fresh_xv infer_e_appPI check_v_wf by blast
    thus  "atom x' ♯ Γ'[x::=v]Γv @ Γ" using infer_e_appPI fresh_subst_gv  wfD_wf subst_g_inside fresh_Pair by metis
    show "τ'[bv::=b']b[x'::=v'[x::=v]vv]v = τ[x::=v]τv"  using  infer_e_appPI subst_tv_commute[OF * ] subst_defs by metis
    show "atom bv ♯ (Θ, Φ, ℬ, Γ'[x::=v]Γv @ Γ, Δ[x::=v]Δv, b', v'[x::=v]vv, τ[x::=v]τv)" 
      by (fresh_mth add: infer_e_appPI fresh_subst_gv_inside)     
  qed
next
  case (infer_e_fstI Θ ℬ Γ'' Δ Φ v' z' b1 b2 c z)

  hence zf: "atom z ♯ CE_fst [v']ce" using ce.fresh e.fresh opp.fresh by metis

  obtain z3'::x where *:"atom z3' ♯ (x,v,AE_fst v', CE_fst [v']ce , AE_fst v'[x::=v]vv ,Γ'[x::=v]Γv @ Γ )" using obtain_fresh by auto
  hence  **:"(⦃ z : b1  | CE_val (V_var z)  ==  CE_fst [v']ce  ⦄) = ⦃ z3' : b1  | CE_val (V_var z3')  ==  CE_fst [v']ce  ⦄" 
    using type_e_eq  infer_e_fstI(4) fresh_Pair zf by metis

  obtain z1' b1' c1' where  z1:"atom z1' ♯ (x,v) ∧ ⦃ z' : B_pair b1 b2 | c ⦄ = ⦃ z1' : b1' | c1' ⦄" using obtain_fresh_z by metis

  have bb:"b1' = B_pair b1 b2" using z1 τ.eq_iff by metis
  have "Θ ; Φ ; ℬ ; Γ'[x::=v]Γv @ Γ ; Δ[x::=v]Δv   ⊢ (AE_fst v'[x::=v]vv)  ⇒ ⦃ z3' : b1  | CE_val (V_var z3')  ==  CE_fst [v'[x::=v]vv]ce  ⦄"
  proof 
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv › using wfD_subst infer_e_fstI  subtype_eq_base2 b_of.simps by metis
    show ‹ Θ⊢wf Φ › using  infer_e_fstI by metis
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇒ ⦃ z1' : B_pair b1 b2 | c1'[x::=v]cv ⦄› using subst_tv.simps subst_infer_v infer_e_fstI z1 bb by metis

    show ‹atom z3' ♯ AE_fst v'[x::=v]vv › using fresh_Pair * by metis
    show ‹atom z3' ♯ Γ'[x::=v]Γv @ Γ› using * by auto
  qed
  moreover have "⦃ z3' : b1  | CE_val (V_var z3')  ==  CE_fst [v'[x::=v]vv]ce ⦄ = ⦃ z3' : b1  | CE_val (V_var z3')  ==  CE_fst [v']ce  ⦄[x::=v]τv"
    using subst_tv.simps subst_ev.simps * by auto
  ultimately show ?case using subst_ev.simps * ** by metis 
next
  case (infer_e_sndI Θ ℬ Γ'' Δ Φ v' z' b1 b2 c z)
  hence zf: "atom z ♯ CE_snd [v']ce" using ce.fresh e.fresh opp.fresh by metis

  obtain z3'::x where *:"atom z3' ♯ (x,v,AE_snd v', CE_snd [v']ce , AE_snd v'[x::=v]vv ,Γ'[x::=v]Γv @ Γ ,v', Γ'')" using obtain_fresh by auto
  hence  **:"(⦃ z : b2  | CE_val (V_var z)  ==  CE_snd [v']ce  ⦄) = ⦃ z3' : b2  | CE_val (V_var z3')  ==  CE_snd [v']ce  ⦄" 
    using type_e_eq  infer_e_sndI(4) fresh_Pair zf by metis

  obtain z1' b2' c1' where  z1:"atom z1' ♯ (x,v) ∧ ⦃ z' : B_pair b1 b2 | c ⦄ = ⦃ z1' : b2' | c1' ⦄" using obtain_fresh_z by metis

  have bb:"b2' = B_pair b1 b2" using z1 τ.eq_iff by metis

  have "Θ ; Φ ; ℬ ; Γ'[x::=v]Γv @ Γ ; Δ[x::=v]Δv   ⊢ (AE_snd (v'[x::=v]vv))  ⇒ ⦃ z3' : b2  | CE_val (V_var z3')  ==  CE_snd ([v'[x::=v]vv]ce)  ⦄"
  proof 
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv › using wfD_subst infer_e_sndI  subtype_eq_base2 b_of.simps by metis
    show ‹ Θ⊢wf Φ › using  infer_e_sndI by metis
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇒ ⦃ z1' : B_pair b1 b2 | c1'[x::=v]cv ⦄› using subst_tv.simps subst_infer_v infer_e_sndI z1 bb by metis

    show ‹atom z3' ♯ AE_snd v'[x::=v]vv › using fresh_Pair * by metis
    show ‹atom z3' ♯ Γ'[x::=v]Γv @ Γ› using * by auto
  qed
  moreover have "⦃ z3' : b2  | CE_val (V_var z3')  ==  CE_snd ([v'[x::=v]vv]ce) ⦄ = ⦃ z3' : b2  | CE_val (V_var z3')  ==  CE_snd [v']ce  ⦄[x::=v]τv"
    by(subst subst_tv.simps, auto simp add: fresh_prodN *)
  ultimately show ?case using subst_ev.simps * ** by metis 
next
  case (infer_e_lenI Θ ℬ Γ'' Δ Φ v' z' c z)
  hence zf: "atom z ♯ CE_len [v']ce" using ce.fresh e.fresh opp.fresh by metis
  obtain z3'::x where *:"atom z3' ♯ (x,v,AE_len v', CE_len [v']ce , AE_len v'[x::=v]vv ,Γ'[x::=v]Γv @ Γ , Γ'',v')" using obtain_fresh by auto
  hence  **:"(⦃ z : B_int  | CE_val (V_var z)  ==  CE_len [v']ce  ⦄) = ⦃ z3' : B_int  | CE_val (V_var z3')  ==  CE_len [v']ce  ⦄" 
    using type_e_eq  infer_e_lenI fresh_Pair zf by metis

  have ***: "Θ ; ℬ ; Γ''  ⊢ v' ⇒ ⦃ z3' : B_bitvec  | CE_val (V_var z3') == CE_val v' ⦄" 
    using infer_e_lenI infer_v_form3[OF infer_e_lenI(3), of z3'] b_of.simps * fresh_Pair by metis

  have "Θ ; Φ ; ℬ ; Γ'[x::=v]Γv @ Γ ; Δ[x::=v]Δv   ⊢ (AE_len (v'[x::=v]vv))  ⇒ ⦃ z3' : B_int | CE_val (V_var z3')  ==  CE_len ([v'[x::=v]vv]ce)  ⦄" 
  proof
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv ›  using wfD_subst infer_e_lenI  subtype_eq_base2 b_of.simps by metis
    show ‹ Θ⊢wf Φ › using  infer_e_lenI by metis

    have ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇒ ⦃ z3' : B_bitvec  | CE_val (V_var z3')  ==  CE_val v'  ⦄[x::=v]τv› 
    proof(rule subst_infer_v)
      show ‹ Θ ; ℬ ; Γ ⊢ v ⇒ τ1› using infer_e_lenI by metis
      show  ‹ Θ ; ℬ ; Γ' @ (x, b1, c0[z0::=[ x ]v]cv) #Γ Γ ⊢ v' ⇒ ⦃ z3' : B_bitvec  | [ [ z3' ]v ]ce  ==  [ v' ]ce  ⦄› using *** infer_e_lenI by metis
      show "Θ ; ℬ ; Γ  ⊢ τ1 ≲ ⦃ z0 : b1  | c0 ⦄" using infer_e_lenI by metis
      show "atom z0 ♯ (x, v)" using infer_e_lenI by metis
    qed

    thus  ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v'[x::=v]vv ⇒ ⦃ z3' : B_bitvec  | CE_val (V_var z3')  ==  CE_val v'[x::=v]vv  ⦄› 
      using  subst_tv.simps subst_ev.simps fresh_Pair * fresh_prodN subst_vv.simps by auto

    show ‹atom z3' ♯ AE_len v'[x::=v]vv› using fresh_Pair * by metis
    show ‹atom z3' ♯ Γ'[x::=v]Γv @ Γ› using fresh_Pair * by metis
  qed

  moreover have "⦃ z3' : B_int | CE_val (V_var z3')  ==  CE_len ([v'[x::=v]vv]ce) ⦄ = ⦃ z3' : B_int  | CE_val (V_var z3')  ==  CE_len [v']ce  ⦄[x::=v]τv"
    using subst_tv.simps subst_ev.simps * by auto

  ultimately show ?case using subst_ev.simps *  ** by metis 
next
  case (infer_e_mvarI Θ ℬ Γ'' Φ Δ u τ)

  have "Θ ; Φ ; ℬ ; Γ'[x::=v]Γv @ Γ ; Δ[x::=v]Δv   ⊢ (AE_mvar u) ⇒ τ[x::=v]τv" 
  proof
    show ‹ Θ ; ℬ⊢wf Γ'[x::=v]Γv @ Γ›  proof - 
      have "wfV Θ ℬ Γ v (b_of τ1)" using infer_v_wf infer_e_mvarI by auto
      moreover have "b_of τ1 = b1" using subtype_eq_base2 infer_e_mvarI b_of.simps by simp
      ultimately show ?thesis using wf_subst(3)[OF infer_e_mvarI(1), of Γ' x b1 "c0[z0::=[x]v]cv" Γ v] infer_e_mvarI subst_g_inside by metis
    qed
    show ‹ Θ⊢wf Φ › using infer_e_mvarI  by auto
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv › using wfD_subst infer_e_mvarI  subtype_eq_base2 b_of.simps by metis
    show ‹(u, τ[x::=v]τv) ∈ setD Δ[x::=v]Δv›  using infer_e_mvarI  subst_dv_member by metis
  qed
  moreover have " (AE_mvar u) =  (AE_mvar u)[x::=v]ev" using subst_ev.simps by auto
  ultimately show ?case by auto

next
  case (infer_e_concatI Θ ℬ Γ'' Δ Φ v1 z1 c1 v2 z2 c2 z3)

  hence zf: "atom z3 ♯ CE_concat [v1]ce [v2]ce" using ce.fresh e.fresh opp.fresh by metis 

  obtain z3'::x where *:"atom z3' ♯ (x,v,v1,v2,AE_concat v1 v2, CE_concat [v1]ce [v2]ce , AE_concat (v1[x::=v]vv) (v2[x::=v]vv) ,Γ'[x::=v]Γv @ Γ , Γ'',v1 , v2)" using obtain_fresh by auto

  hence  **:"(⦃ z3 : B_bitvec  | CE_val (V_var z3)  ==  CE_concat [v1]ce [v2]ce ⦄) = ⦃ z3' : B_bitvec  | CE_val (V_var z3')  ==  CE_concat [v1]ce [v2]ce  ⦄" 
    using type_e_eq  infer_e_concatI fresh_Pair zf by metis
  have zfx: "atom x ♯ z3'"  using fresh_at_base fresh_prodN * by auto

  have v1: "Θ ; ℬ ; Γ''  ⊢ v1 ⇒ ⦃ z3' : B_bitvec  | CE_val (V_var z3') == CE_val v1 ⦄" 
    using infer_e_concatI infer_v_form3 b_of.simps * fresh_Pair by metis
  have v2: "Θ ; ℬ ; Γ''  ⊢ v2 ⇒ ⦃ z3' : B_bitvec  | CE_val (V_var z3') == CE_val v2 ⦄" 
    using infer_e_concatI infer_v_form3 b_of.simps * fresh_Pair by metis

  have "Θ ; Φ ; ℬ ; Γ'[x::=v]Γv @ Γ ; Δ[x::=v]Δv   ⊢ (AE_concat (v1[x::=v]vv) (v2[x::=v]vv))  ⇒ ⦃ z3' : B_bitvec | CE_val (V_var z3')  ==  CE_concat ([v1[x::=v]vv]ce) ([v2[x::=v]vv]ce)  ⦄" 
  proof
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv ›  using wfD_subst infer_e_concatI  subtype_eq_base2 b_of.simps by metis
    show ‹ Θ⊢wf Φ › by(simp add: infer_e_concatI) 
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v1[x::=v]vv ⇒ ⦃ z3' : B_bitvec  | CE_val (V_var z3')  ==  CE_val (v1[x::=v]vv)  ⦄›
      using subst_infer_v_form infer_e_concatI fresh_prodN * b_of.simps by metis
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ  ⊢ v2[x::=v]vv ⇒ ⦃ z3' : B_bitvec  | CE_val (V_var z3')  ==  CE_val (v2[x::=v]vv)  ⦄›   
      using subst_infer_v_form infer_e_concatI fresh_prodN * b_of.simps by metis
    show ‹atom z3' ♯ AE_concat v1[x::=v]vv  v2[x::=v]vv› using fresh_Pair * by metis
    show ‹atom z3' ♯ Γ'[x::=v]Γv @ Γ› using fresh_Pair * by metis
  qed

  moreover have "⦃ z3' : B_bitvec | CE_val (V_var z3')  ==  CE_concat ([v1[x::=v]vv]ce) ([v2[x::=v]vv]ce) ⦄ = ⦃ z3' : B_bitvec  | CE_val (V_var z3')  ==  CE_concat [v1]ce [v2]ce  ⦄[x::=v]τv"
    using subst_tv.simps subst_ev.simps * by auto

  ultimately show ?case using subst_ev.simps ** * by metis
next
  case (infer_e_splitI Θ ℬ Γ'' Δ Φ v1 z1 c1 v2 z2 z3)
  hence *:"atom z3 ♯ (x,v)" using fresh_Pair by auto
  have ‹x ≠ z3 › using infer_e_splitI by force
  have "Θ ; Φ ; ℬ ; (Γ'[x::=v]Γv @ Γ) ; Δ[x::=v]Δv  ⊢ (AE_split v1[x::=v]vv v2[x::=v]vv) ⇒ 
               ⦃ z3 : [ B_bitvec , B_bitvec ]b  | [ v1[x::=v]vv ]ce  ==  [ [#1[ [ z3 ]v ]ce]ce @@ [#2[ [ z3 ]v ]ce]ce ]ce   AND  
                     [| [#1[ [ z3 ]v ]ce]ce |]ce  ==  [ v2[x::=v]vv ]ce   ⦄"
  proof
    show ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢wf Δ[x::=v]Δv ›  using wfD_subst infer_e_splitI  subtype_eq_base2 b_of.simps by metis
    show ‹ Θ  ⊢wf Φ › using infer_e_splitI by auto
    have  ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ v1[x::=v]vv ⇒ ⦃ z1 : B_bitvec  | c1 ⦄[x::=v]τv› 
      using subst_infer_v infer_e_splitI by metis
    thus ‹ Θ ; ℬ ; Γ'[x::=v]Γv @ Γ ⊢ v1[x::=v]vv ⇒ ⦃ z1 : B_bitvec  | c1[x::=v]cv ⦄› 
      using infer_e_splitI subst_tv.simps fresh_Pair by metis
    have ‹x ≠ z2 › using infer_e_splitI by force
    have "(⦃ z2 : B_int  | ([ leq [ [ L_num 0 ]v ]ce [ [ z2 ]v ]ce ]ce  ==  [ [ L_true ]v ]ce)   
                     AND  ([ leq [ [ z2 ]v ]ce [| [ v1[x::=v]vv ]ce |]ce ]ce  ==  [ [ L_true ]v ]ce )  ⦄) = 
         (⦃ z2 : B_int  | ([ leq [ [ L_num  0 ]v ]ce [ [ z2 ]v ]ce ]ce  ==  [ [ L_true ]v ]ce )  
                     AND  ([ leq [ [ z2 ]v ]ce [| [ v1 ]ce |]ce ]ce  ==  [ [ L_true ]v ]ce )  ⦄[x::=v]τv)"
      unfolding subst_cv.simps subst_cev.simps subst_vv.simps using ‹x ≠ z2› infer_e_splitI fresh_Pair by simp
    thus  ‹Θ ; ℬ ; Γ'[x::=v]Γv @
                 Γ  ⊢ v2[x::=v]vv ⇐ ⦃ z2 : B_int  | [ leq [ [ L_num 0 ]v ]ce [ [ z2 ]v ]ce ]ce  ==  [ [ L_true ]v ]ce   
                     AND  [ leq [ [ z2 ]v ]ce [| [ v1[x::=v]vv ]ce |]ce ]ce  ==  [ [ L_true ]v ]ce   ⦄›
      using infer_e_splitI  subst_infer_check_v fresh_Pair by metis

    show ‹atom z1 ♯ AE_split v1[x::=v]vv v2[x::=v]vv› using infer_e_splitI fresh_subst_vv_if by auto
    show ‹atom z2 ♯ AE_split v1[x::=v]vv v2[x::=v]vv› using infer_e_splitI fresh_subst_vv_if by auto
    show ‹atom z3 ♯ AE_split v1[x::=v]vv v2[x::=v]vv› using infer_e_splitI fresh_subst_vv_if by auto

    show ‹atom z3 ♯ Γ'[x::=v]Γv @ Γ›  using   fresh_subst_gv_inside infer_e_splitI by metis
    show ‹atom z2 ♯ Γ'[x::=v]Γv @ Γ›  using   fresh_subst_gv_inside infer_e_splitI by metis
    show ‹atom z1 ♯ Γ'[x::=v]Γv @ Γ›  using   fresh_subst_gv_inside infer_e_splitI by metis
  qed
  thus ?case apply (subst subst_tv.simps)
    using infer_e_splitI fresh_Pair apply metis
    unfolding subst_tv.simps subst_ev.simps subst_cv.simps subst_cev.simps subst_vv.simps * 
    using ‹x ≠ z3› by simp
qed

lemma infer_e_uniqueness:
  assumes "Θ ; Φ ; ℬ ; GNil ; Δ  ⊢ e1 ⇒ τ1" and "Θ ; Φ ; ℬ ; GNil ; Δ  ⊢ e1 ⇒ τ2"
  shows "τ1 = τ2"
  using assms proof(nominal_induct rule:e.strong_induct)
  case (AE_val x)
  then show ?case using infer_e_elims(7)[OF AE_val(1)] infer_e_elims(7)[OF AE_val(2)] infer_v_uniqueness by metis
next
  case (AE_app f v)

  obtain x1 b1 c1 s1' τ1' where t1: "Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x1 b1 c1 τ1' s1'))) = lookup_fun Φ f ∧  τ1 = τ1'[x1::=v]τv" using  infer_e_app2E[OF AE_app(1)] by metis
  moreover obtain x2 b2 c2 s2' τ2' where t2: "Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x2 b2 c2 τ2' s2'))) = lookup_fun Φ f ∧  τ2 = τ2'[x2::=v]τv" using  infer_e_app2E[OF AE_app(2)] by metis

  have "τ1'[x1::=v]τv = τ2'[x2::=v]τv" using t1 and t2  fun_ret_unique by metis
  thus ?thesis using t1 t2 by auto
next
  case (AE_appP f b v)
  obtain bv1 x1 b1 c1 s1' τ1' where t1: "Some (AF_fundef f (AF_fun_typ_some bv1 (AF_fun_typ x1 b1 c1 τ1' s1'))) = lookup_fun Φ f ∧  τ1 = τ1'[bv1::=b]τb[x1::=v]τv" using  infer_e_appP2E[OF AE_appP(1)] by metis
  moreover obtain bv2 x2 b2 c2 s2' τ2' where t2: "Some (AF_fundef f (AF_fun_typ_some bv2 (AF_fun_typ x2 b2 c2 τ2' s2'))) = lookup_fun Φ f ∧  τ2 = τ2'[bv2::=b]τb[x2::=v]τv" using  infer_e_appP2E[OF AE_appP(2)] by metis

  have "τ1'[bv1::=b]τb[x1::=v]τv = τ2'[bv2::=b]τb[x2::=v]τv" using t1 and t2  fun_poly_ret_unique by metis
  thus ?thesis using t1 t2 by auto
next
  case (AE_op opp v1 v2)
  show ?case proof(rule opp.exhaust)
    assume "opp = plus"
    hence "Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op Plus v1 v2 ⇒ τ1" and  "Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op Plus v1 v2 ⇒ τ2" using AE_op by auto
    thus ?thesis using infer_e_elims(11)[OF ‹Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op Plus v1 v2 ⇒ τ1› ] infer_e_elims(11)[OF ‹Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op Plus v1 v2 ⇒ τ2› ]
      by force
  next
    assume "opp = leq"
    hence "opp = LEq" using opp.strong_exhaust by auto
    hence "Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op LEq v1 v2 ⇒ τ1" and  "Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op LEq v1 v2 ⇒ τ2" using AE_op by auto
    thus ?thesis using infer_e_elims(12)[OF ‹Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op LEq v1 v2 ⇒ τ1› ] infer_e_elims(12)[OF ‹Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op LEq v1 v2 ⇒ τ2› ]
      by force
  next
    assume "opp = eq"
    hence "opp = Eq" using opp.strong_exhaust by auto
    hence "Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op Eq v1 v2 ⇒ τ1" and  "Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op Eq v1 v2 ⇒ τ2" using AE_op by auto
    thus ?thesis using infer_e_elims(25)[OF ‹Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op Eq v1 v2 ⇒ τ1› ] infer_e_elims(25)[OF ‹Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AE_op Eq v1 v2 ⇒ τ2› ]
      by force
  qed
next
  case (AE_concat v1 v2)

  obtain z3::x where t1:"τ1 = ⦃ z3 : B_bitvec  | [ [ z3 ]v ]ce  ==  CE_concat [v1]ce [v2]ce  ⦄ ∧ atom z3 ♯ v1 ∧ atom z3 ♯ v2 " using infer_e_elims(18)[OF AE_concat(1)] by metis
  obtain z3'::x where t2:"τ2 = ⦃ z3' : B_bitvec  | [ [ z3' ]v ]ce  ==  CE_concat [v1]ce [v2]ce  ⦄ ∧ atom z3' ♯ v1 ∧ atom z3' ♯ v2" using infer_e_elims(18)[OF AE_concat(2)] by metis

  thus ?case using t1 t2 type_e_eq ce.fresh by metis

next
  case (AE_fst v)

  obtain z1 and b1 where "τ1 = ⦃ z1 : b1  | CE_val (V_var z1)  ==  (CE_fst [v]ce)  ⦄" using infer_v_form AE_fst by auto

  obtain xx :: x and bb :: b and xxa :: x and bba :: b and cc :: c where
    f1: "τ2 = ⦃ xx : bb | CE_val (V_var xx) == CE_fst [v]ce ⦄ ∧ Θ ; ℬ ; GNil⊢wf Δ ∧ Θ ; ℬ ; GNil ⊢ v ⇒ ⦃ xxa : B_pair bb bba | cc ⦄ ∧ atom xx ♯ v"
    using infer_e_elims(8)[OF AE_fst(2)] by metis
  obtain xxb :: x and bbb :: b and xxc :: x and bbc :: b and cca :: c where
    f2: "τ1 = ⦃ xxb : bbb | CE_val (V_var xxb) == CE_fst [v]ce ⦄ ∧ Θ ; ℬ ; GNil⊢wf Δ ∧ Θ ; ℬ ; GNil ⊢ v ⇒ ⦃ xxc : B_pair bbb bbc | cca ⦄ ∧ atom xxb ♯ v"
    using infer_e_elims(8)[OF AE_fst(1)] by metis
  then have "B_pair bb bba = B_pair bbb bbc"
    using f1 by (metis (no_types) b_of.simps infer_v_uniqueness) 
  then have "⦃ xx : bbb | CE_val (V_var xx) == CE_fst [v]ce ⦄ = τ2"
    using f1 by auto 
  then show ?thesis
    using f2 by (meson ce.fresh fresh_GNil type_e_eq wfG_x_fresh_in_v_simple) 
next
  case (AE_snd v)
  obtain xx :: x and bb :: b and xxa :: x and bba :: b and cc :: c where
    f1: "τ2 = ⦃ xx : bba | CE_val (V_var xx) == CE_snd [v]ce ⦄ ∧ Θ ; ℬ ; GNil⊢wf Δ ∧ Θ ; ℬ ; GNil ⊢ v ⇒ ⦃ xxa : B_pair bb bba | cc ⦄ ∧ atom xx ♯ v"
    using infer_e_elims(9)[OF AE_snd(2)] by metis
  obtain xxb :: x and bbb :: b and xxc :: x and bbc :: b and cca :: c where
    f2: "τ1 = ⦃ xxb : bbc | CE_val (V_var xxb) == CE_snd [v]ce ⦄ ∧ Θ ; ℬ ; GNil⊢wf Δ ∧ Θ ; ℬ ; GNil ⊢ v ⇒ ⦃ xxc : B_pair bbb bbc | cca ⦄ ∧ atom xxb ♯ v"
    using infer_e_elims(9)[OF AE_snd(1)] by metis
  then have "B_pair bb bba = B_pair bbb bbc"
    using f1 by (metis (no_types) b_of.simps infer_v_uniqueness) 
  then have "⦃ xx : bbc | CE_val (V_var xx) == CE_snd [v]ce ⦄ = τ2"
    using f1 by auto 
  then show ?thesis
    using f2 by (meson ce.fresh fresh_GNil type_e_eq wfG_x_fresh_in_v_simple) 
next
  case (AE_mvar x)
  then show ?case using infer_e_elims(10)[OF AE_mvar(1)] infer_e_elims(10)[OF AE_mvar(2)] wfD_unique   by metis
next
  case (AE_len x)
  then show ?case using infer_e_elims(16)[OF AE_len(1)] infer_e_elims(16)[OF AE_len(2)] by force
next
  case (AE_split x1a x2)
  then show ?case using infer_e_elims(22)[OF AE_split(1)] infer_e_elims(22)[OF AE_split(2)] by force
qed

section ‹Statements›

lemma subst_infer_check_v1:
  fixes v::v and v'::v and Γ::Γ
  assumes "Γ = Γ1@((x,b1,c0[z0::=[x]v]cv)#ΓΓ2)"  and 
    "Θ ; ℬ ; Γ2 ⊢ v ⇒ τ1"  and
    "Θ ; ℬ ; Γ ⊢ v' ⇐ τ2"  and
    "Θ ; ℬ ; Γ2 ⊢ τ1 ≲  ⦃ z0 : b1 | c0 ⦄" and "atom z0 ♯ (x,v)"
  shows "Θ ; ℬ  ; Γ[x::=v]Γv ⊢  v'[x::=v]vv ⇐ τ2[x::=v]τv"
  using  subst_g_inside check_v_wf assms subst_infer_check_v by metis

lemma infer_v_c_valid:
  assumes " Θ ; ℬ ; Γ ⊢ v ⇒ τ"  and   "Θ ; ℬ ; Γ  ⊢ τ ≲ ⦃ z : b  | c ⦄"
  shows  ‹Θ ; ℬ ; Γ  ⊨ c[z::=v]cv ›
proof -
  obtain z1 and b1 and c1 where *:"τ = ⦃ z1 : b1 | c1 ⦄ ∧ atom z1 ♯ (c,v,Γ)" using obtain_fresh_z by metis
  then have "b1 = b" using assms subtype_eq_base by metis
  moreover then have "Θ ; ℬ ; Γ ⊢ v ⇒ ⦃ z1 : b | c1 ⦄" using assms * by auto

  moreover have "Θ ; ℬ ; (z1, b, c1) #Γ Γ  ⊨ c[z::=[ z1 ]v]cv " proof -
    have "Θ ; ℬ ; (z1, b, c1[z1::=[ z1 ]v]v) #Γ Γ  ⊨ c[z::=[ z1 ]v]v "
      using subtype_valid[OF assms(2), of z1 z1 b c1 z c ] * fresh_prodN ‹b1 = b› by metis
    moreover have "c1[z1::=[ z1 ]v]v = c1" using subst_v_v_def by simp
    ultimately show ?thesis using subst_v_c_def by metis
  qed
  ultimately show ?thesis using * fresh_prodN subst_valid_simple by metis
qed

text ‹ Substitution Lemma for Statements ›

lemma subst_infer_check_s:
  fixes v::v and s::s and cs::branch_s and x::x and c::c and b::b and 
    Γ1::Γ and Γ2::Γ and css::branch_list
  assumes "Θ ; ℬ ; Γ1 ⊢ v ⇒ τ"  and "Θ ; ℬ ; Γ1 ⊢ τ ≲ ⦃ z : b | c ⦄"  and
    "atom z ♯ (x, v)"
  shows  "Θ ; Φ ; ℬ ; Γ; Δ  ⊢ s ⇐  τ'   ⟹ 
          Γ = (Γ2@((x,b,c[z::=[x]v]cv)#ΓΓ1)) ⟹ 
          Θ ; Φ ; ℬ ; Γ[x::=v]Γv ; Δ[x::=v]Δv ⊢ s[x::=v]sv  ⇐ τ'[x::=v]τv" 
    and 
    "Θ ; Φ ; ℬ ; Γ; Δ; tid ; cons ; const ; v' ⊢ cs ⇐ τ' ⟹ 
          Γ = (Γ2@((x,b,c[z::=[x]v]cv)#ΓΓ1)) ⟹ 
          Θ ; Φ ; ℬ ; Γ[x::=v]Γv ; Δ[x::=v]Δv; 
          tid ; cons ; const ; v'[x::=v]vv ⊢ cs[x::=v]sv ⇐ τ'[x::=v]τv" 
    and
    "Θ ; Φ ; ℬ ; Γ; Δ; tid ; dclist ; v' ⊢ css ⇐ τ' ⟹ 
         Γ = (Γ2@((x,b,c[z::=[x]v]cv)#ΓΓ1)) ⟹ 
         Θ ; Φ ; ℬ ; Γ[x::=v]Γv ; Δ[x::=v]Δv; tid ; dclist ; v'[x::=v]vv ⊢ 
             subst_branchlv css x v  ⇐ τ'[x::=v]τv"

  using assms proof(nominal_induct τ' and τ' and τ' avoiding: x v arbitrary: Γ2 and Γ2  and Γ2 
    rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_valI Θ  ℬ Γ Δ  Φ  v' τ' τ'')

  have sg: " Γ[x::=v]Γv = Γ2[x::=v]Γv@Γ1" using  check_valI  by subst_mth
  have "Θ ; Φ ; ℬ ; Γ[x::=v]Γv ; Δ[x::=v]Δv  ⊢ (AS_val (v'[x::=v]vv)) ⇐ τ''[x::=v]τv" proof
    have "Θ ; ℬ ; Γ1⊢wf v : b " using infer_v_v_wf subtype_eq_base2 b_of.simps check_valI by metis
    thus  ‹Θ ; ℬ ; Γ[x::=v]Γv⊢wf Δ[x::=v]Δv›  using wf_subst(15) check_valI by auto
    show ‹ Θ⊢wf Φ › using check_valI by auto
    show ‹ Θ ; ℬ ; Γ[x::=v]Γv  ⊢ v'[x::=v]vv ⇒ τ'[x::=v]τv› proof(subst sg, rule subst_infer_v)
      show "Θ ; ℬ ; Γ1 ⊢ v ⇒ τ" using check_valI by auto
      show "Θ ; ℬ ; Γ2 @ (x, b, c[z::=[x]v]cv) #Γ Γ1 ⊢ v' ⇒ τ'"  using check_valI by metis
      show "Θ ; ℬ ; Γ1  ⊢ τ ≲ ⦃ z: b   | c ⦄" using check_valI by auto
      show "atom z ♯ (x, v)" using check_valI by auto
    qed
    show ‹Θ ; ℬ ; Γ[x::=v]Γv  ⊢  τ'[x::=v]τv ≲ τ''[x::=v]τv› using subst_subtype_tau check_valI sg by metis
  qed

  thus  ?case using Typing.check_valI subst_sv.simps sg by auto
next
  case (check_letI xa Θ Φ ℬ Γ Δ ea τa za sa ba ca)
  have *:"(AS_let xa ea sa)[x::=v]sv=(AS_let xa (ea[x::=v]ev) sa[x::=v]sv)" 
    using subst_sv.simps ‹ atom xa ♯ x›  ‹ atom xa ♯ v› by auto
  show ?case unfolding * proof

    show "atom xa ♯ (Θ,Φ,ℬ,Γ[x::=v]Γv,Δ[x::=v]Δv,ea[x::=v]ev,τa[x::=v]τv)"
      by(subst_tuple_mth add: check_letI)

    show  "atom za ♯ (xa,Θ,Φ,ℬ,Γ[x::=v]Γv, Δ[x::=v]Δv,ea[x::=v]ev,
                         τa[x::=v]τv,sa[x::=v]sv)"
      by(subst_tuple_mth add: check_letI)

    show "Θ; Φ; ℬ; Γ[x::=v]Γv; Δ[x::=v]Δv ⊢ 
                          ea[x::=v]ev ⇒  ⦃ za : ba | ca[x::=v]cv ⦄" 
    proof - 
      have "Θ; Φ; ℬ; Γ2[x::=v]Γv @ Γ1; Δ[x::=v]Δv ⊢ 
                          ea[x::=v]ev ⇒ ⦃ za : ba | ca ⦄[x::=v]τv" 
        using check_letI subst_infer_e by metis
      thus ?thesis using check_letI subst_tv.simps 
        by (metis fresh_prod2I infer_e_wf subst_g_inside_simple)
    qed

    show  "Θ; Φ; ℬ; (xa, ba, ca[x::=v]cv[za::=V_var xa]v) #Γ Γ[x::=v]Γv;
                          Δ[x::=v]Δv  ⊢ sa[x::=v]sv ⇐ τa[x::=v]τv" 
    proof -   
      have "Θ; Φ; ℬ; ((xa, ba, ca[za::=V_var xa]v) #Γ Γ)[x::=v]Γv ; 
                          Δ[x::=v]Δv  ⊢  sa[x::=v]sv ⇐ τa[x::=v]τv" 
        apply(rule check_letI(23)[of "(xa, ba, ca[za::=V_var xa]cv) #Γ Γ2"])
        by(metis check_letI append_g.simps subst_defs)+

      moreover have "(xa, ba, ca[x::=v]cv[za::=V_var xa]cv) #Γ Γ[x::=v]Γv = 
                     ((xa, ba, ca[za::=V_var xa]cv) #Γ Γ)[x::=v]Γv" 
        using subst_cv_commute subst_gv.simps check_letI 
        by (metis ms_fresh_all(39) ms_fresh_all(49) subst_cv_commute_full)
      ultimately show ?thesis 
        using subst_defs by  auto      
    qed
  qed
next
  case (check_assertI xa Θ Φ ℬ Γ Δ ca τ s)
  show ?case unfolding subst_sv.simps proof  
    show ‹atom xa ♯ (Θ, Φ, ℬ, Γ[x::=v]Γv, Δ[x::=v]Δv, ca[x::=v]cv, τ[x::=v]τv, s[x::=v]sv)› 
      by(subst_tuple_mth add: check_assertI)
    have "xa ≠ x" using check_assertI by fastforce
    thus ‹ Θ ; Φ ; ℬ ; (xa, B_bool, ca[x::=v]cv) #Γ Γ[x::=v]Γv ; Δ[x::=v]Δv  ⊢ s[x::=v]sv ⇐ τ[x::=v]τv› 
      using check_assertI(12)[of "(xa, B_bool, c) #Γ Γ2" x v]  check_assertI subst_gv.simps append_g.simps by metis
    have ‹Θ ; ℬ ; Γ2[x::=v]Γv @ Γ1  ⊨ ca[x::=v]cv › proof(rule  subst_valid )
      show   ‹Θ ; ℬ ; Γ1  ⊨ c[z::=v]cv › using infer_v_c_valid check_assertI by metis
      show ‹ Θ ; ℬ ; Γ1 ⊢wf v : b › using check_assertI infer_v_wf b_of.simps subtype_eq_base 
        by (metis subtype_eq_base2)
      show ‹ Θ ; ℬ  ⊢wf Γ1 › using check_assertI infer_v_wf by metis
      have " Θ ; ℬ  ⊢wf Γ2 @ (x, b, c[z::=[ x ]v]cv) #Γ Γ1" using check_assertI wfX_wfY by metis
      thus  ‹atom x ♯ Γ1› using check_assertI wfG_suffix wfG_elims by metis    

      moreover have "Θ ; ℬ ; Γ1 ⊢wf  ⦃ z : b  | c ⦄" using subtype_wfT check_assertI by metis
      moreover have "x ≠ z" using fresh_Pair check_assertI fresh_x_neq by metis
      ultimately show  ‹atom x ♯ c› using check_assertI wfT_fresh_c by metis

      show ‹ Θ ; ℬ  ⊢wf Γ2 @ (x, b, c[z::=[ x ]v]cv) #Γ Γ1 › using check_assertI wfX_wfY by metis
      show ‹Θ ; ℬ ; Γ2 @ (x, b, c[z::=[ x ]v]cv) #Γ Γ1  ⊨ ca › using check_assertI by auto
    qed
    thus  ‹Θ ; ℬ ; Γ[x::=v]Γv  ⊨ ca[x::=v]cv › using check_assertI 
    proof -
      show ?thesis
        by (metis (no_types) ‹Γ = Γ2 @ (x, b, c[z::=[ x ]v]cv) #Γ Γ1› ‹Θ ; ℬ ; Γ ⊨ ca› ‹Θ ; ℬ ; Γ2[x::=v]Γv @ Γ1 ⊨ ca[x::=v]cv› subst_g_inside valid_g_wf) (* 93 ms *)
    qed

    have "Θ ; ℬ ; Γ1 ⊢wf v : b" using infer_v_wf b_of.simps check_assertI 
      by (metis subtype_eq_base2)
    thus  ‹ Θ ; ℬ ; Γ[x::=v]Γv ⊢wf Δ[x::=v]Δv › using wf_subst2(6) check_assertI by metis
  qed
next
  case (check_branch_list_consI Θ Φ ℬ Γ Δ tid dclist vv cs τ css)  
  show ?case unfolding * using subst_sv.simps check_branch_list_consI by simp
next
  case (check_branch_list_finalI Θ Φ ℬ Γ Δ tid dclist v cs τ)
  show ?case unfolding * using subst_sv.simps check_branch_list_finalI by simp
next
  case (check_branch_s_branchI Θ ℬ Γ Δ τ const xa Φ tid cons va sa)
  hence *:"(AS_branch cons xa sa)[x::=v]sv = (AS_branch cons xa sa[x::=v]sv)" using subst_branchv.simps fresh_Pair by metis
  show ?case unfolding *  proof

    show "Θ ; ℬ ; Γ[x::=v]Γv⊢wf Δ[x::=v]Δv "   
      using wf_subst check_branch_s_branchI subtype_eq_base2 b_of.simps infer_v_wf by metis 

    show  "⊢wf Θ " using check_branch_s_branchI by metis

    show  "Θ ; ℬ ; Γ[x::=v]Γv  ⊢wf τ[x::=v]τv " 
      using wf_subst check_branch_s_branchI subtype_eq_base2 b_of.simps infer_v_wf by metis 

    show wft:"Θ ; {||} ; GNil⊢wf const "  using check_branch_s_branchI by metis

    show "atom xa ♯ (Θ, Φ, ℬ, Γ[x::=v]Γv, Δ[x::=v]Δv, tid, cons, const,va[x::=v]vv, τ[x::=v]τv)"
      apply(unfold fresh_prodN, (simp add: check_branch_s_branchI )+)
      apply(rule,metis fresh_z_subst_g check_branch_s_branchI fresh_Pair )
      by(metis fresh_subst_dv check_branch_s_branchI fresh_Pair )  

    have "Θ ; Φ ; ℬ ; ((xa, b_of const, CE_val va  ==  CE_val(V_cons tid cons (V_var xa))   AND c_of const xa) #Γ Γ)[x::=v]Γv ; Δ[x::=v]Δv  ⊢ sa[x::=v]sv ⇐ τ[x::=v]τv" 
      using check_branch_s_branchI   by (metis append_g.simps(2))

    moreover have "(xa, b_of const, CE_val va[x::=v]vv  ==  CE_val (V_cons tid cons (V_var xa))   AND c_of (const) xa) #Γ Γ[x::=v]Γv = 
                  ((xa, b_of const , CE_val va  ==  CE_val (V_cons tid cons (V_var xa)) AND c_of const xa) #Γ Γ)[x::=v]Γv" 
    proof -
      have *:"xa ≠ x" using check_branch_s_branchI fresh_at_base by metis
      have "atom x ♯ const" using wfT_nil_supp[OF wft]  fresh_def by auto
      hence "atom x ♯ (const,xa)" using fresh_at_base wfT_nil_supp[OF wft] fresh_Pair fresh_def * by auto
      moreover hence "(c_of (const) xa)[x::=v]cv =  c_of (const) xa"  
        using c_of_fresh[of x const xa] forget_subst_cv wfT_nil_supp wft by metis
      moreover hence "(V_cons tid cons (V_var xa))[x::=v]vv  = (V_cons tid cons (V_var xa))" using check_branch_s_branchI subst_vv.simps * by metis    
      ultimately show ?thesis using subst_gv.simps check_branch_s_branchI subst_cv.simps subst_cev.simps *  by presburger
    qed

    ultimately show  "Θ ; Φ ; ℬ ; (xa, b_of const, CE_val va[x::=v]vv  ==  CE_val (V_cons tid cons (V_var xa))  AND  c_of const xa) #Γ Γ[x::=v]Γv ; Δ[x::=v]Δv  ⊢ sa[x::=v]sv ⇐ τ[x::=v]τv" 
      by metis
  qed

next
  case (check_let2I xa Θ Φ ℬ G Δ t s1 τa s2 )
  hence *:"(AS_let2 xa t s1 s2)[x::=v]sv = (AS_let2 xa t[x::=v]τv  (s1[x::=v]sv) s2[x::=v]sv)" using subst_sv.simps fresh_Pair by metis
  have "xa ≠ x"  using check_let2I fresh_at_base by metis
  show ?case unfolding * proof
    show "atom xa ♯ (Θ, Φ, ℬ, G[x::=v]Γv, Δ[x::=v]Δv, t[x::=v]τv, s1[x::=v]sv, τa[x::=v]τv)" 
      by(subst_tuple_mth add: check_let2I)    
    show "Θ ; Φ ; ℬ ; G[x::=v]Γv ; Δ[x::=v]Δv  ⊢ s1[x::=v]sv ⇐ t[x::=v]τv" using check_let2I by metis

    have "Θ ; Φ ; ℬ ; ((xa, b_of t, c_of t xa) #Γ G)[x::=v]Γv ; Δ[x::=v]Δv  ⊢ s2[x::=v]sv ⇐ τa[x::=v]τv" 
    proof(rule check_let2I(14))
      show ‹(xa, b_of t, c_of t xa) #Γ G = (((xa, b_of t, c_of t xa)#Γ Γ2)) @ (x, b, c[z::=[ x ]v]cv) #Γ Γ1› 
        using check_let2I append_g.simps by metis
      show ‹ Θ ; ℬ ; Γ1 ⊢ v ⇒ τ› using check_let2I by metis
      show ‹Θ ; ℬ ; Γ1  ⊢ τ ≲ ⦃ z : b  | c ⦄› using check_let2I by metis
      show ‹atom z ♯ (x, v)› using check_let2I by metis
    qed
    moreover  have "c_of t[x::=v]τv xa = (c_of t xa)[x::=v]cv" using subst_v_c_of fresh_Pair check_let2I by metis
    moreover have "b_of t[x::=v]τv = b_of t" using b_of.simps subst_tv.simps b_of_subst by metis
    ultimately show " Θ ; Φ ; ℬ ; (xa, b_of t[x::=v]τv, c_of t[x::=v]τv xa) #Γ G[x::=v]Γv ; Δ[x::=v]Δv  ⊢ s2[x::=v]sv ⇐ τa[x::=v]τv" 
      using check_let2I(14) subst_gv.simps ‹xa ≠ x› b_of.simps by metis
  qed

next

  case (check_varI u Θ Φ ℬ Γ Δ τ' va τ'' s)
  have **: "Γ[x::=v]Γv = Γ2[x::=v]Γv@Γ1" using subst_g_inside check_s_wf check_varI by meson

  have "Θ ; Φ  ;ℬ ; subst_gv Γ x v ; Δ[x::=v]Δv ⊢ AS_var u τ'[x::=v]τv (va[x::=v]vv) (subst_sv s x v) ⇐ τ''[x::=v]τv" 
  proof(rule Typing.check_varI)
    show "atom u ♯ (Θ, Φ, ℬ, Γ[x::=v]Γv, Δ[x::=v]Δv, τ'[x::=v]τv, va[x::=v]vv, τ''[x::=v]τv)" 
      by(subst_tuple_mth add: check_varI)    
    show "Θ ; ℬ ; Γ[x::=v]Γv  ⊢ va[x::=v]vv ⇐ τ'[x::=v]τv" using check_varI subst_infer_check_v ** by metis
    show "Θ ; Φ ; ℬ ; subst_gv Γ x v ; (u, τ'[x::=v]τv) #Δ Δ[x::=v]Δv  ⊢ s[x::=v]sv ⇐ τ''[x::=v]τv" proof - 
      have "wfD Θ ℬ (Γ2 @ (x, b, c[z::=[x]v]cv) #Γ Γ1) ((u,τ')#Δ Δ)" using check_varI check_s_wf  by meson
      moreover have "wfV Θ ℬ Γ1 v (b_of τ)"  using infer_v_wf check_varI(6) check_varI by metis
      have "wfD Θ ℬ (Γ[x::=v]Γv) ((u, τ'[x::=v]τv) #Δ Δ[x::=v]Δv)" proof(subst subst_dv.simps(2)[symmetric], subst **, rule wfD_subst)
        show "Θ ; ℬ ; Γ1 ⊢ v ⇒ τ" using check_varI by auto
        show "Θ ; ℬ ; Γ2 @ (x, b, c[z::=[x]v]cv) #Γ Γ1⊢wf (u, τ') #Δ Δ" using check_varI check_s_wf by simp
        show "b_of τ = b" using check_varI subtype_eq_base2 b_of.simps by auto
      qed
      thus ?thesis using  check_varI by auto
    qed
  qed
  moreover have "atom u ♯ (x,v)" using u_fresh_xv by auto
  ultimately show ?case using subst_sv.simps(7) by auto

next
  case (check_assignI P Φ ℬ Γ Δ u τ1  v' z1 τ')  (* may need to revisit subst in Δ as well *)

  have "wfG P ℬ Γ" using check_v_wf check_assignI by simp
  hence gs: "Γ2[x::=v]Γv @ Γ1 = Γ[x::=v]Γv" using subst_g_inside check_assignI by simp

  have "P ; Φ ; ℬ ; Γ[x::=v]Γv  ; Δ[x::=v]Δv  ⊢ AS_assign u (v'[x::=v]vv) ⇐ τ'[x::=v]τv"
  proof(rule Typing.check_assignI)
    show "P ⊢wf Φ " using check_assignI by auto
    show "wfD P ℬ (Γ[x::=v]Γv) Δ[x::=v]Δv" using wf_subst(15)[OF check_assignI(2)] gs infer_v_v_wf check_assignI b_of.simps subtype_eq_base2 by metis
    thus "(u, τ1[x::=v]τv) ∈ setD Δ[x::=v]Δv" using check_assignI  subst_dv_member by metis
    thus  "P ; ℬ ; Γ[x::=v]Γv  ⊢ v'[x::=v]vv ⇐ τ1[x::=v]τv" using subst_infer_check_v check_assignI gs by metis

    have "P ; ℬ ; Γ2[x::=v]Γv @ Γ1  ⊢ ⦃ z : B_unit  | TRUE ⦄[x::=v]τv ≲ τ'[x::=v]τv" proof(rule subst_subtype_tau)
      show "P ; ℬ ; Γ1  ⊢ v ⇒ τ" using check_assignI by auto
      show "P ; ℬ ; Γ1  ⊢ τ ≲ ⦃ z : b  | c ⦄" using check_assignI by meson
      show "P ; ℬ ; Γ2 @ (x, b, c[z::=[x]v]cv) #Γ Γ1  ⊢ ⦃ z : B_unit  | TRUE ⦄ ≲ τ'" using check_assignI
        by (metis Abs1_eq_iff(3) τ.eq_iff c.fresh(1) c.perm_simps(1))
      show "atom z ♯ (x, v)" using check_assignI by auto
    qed
    moreover have "⦃ z : B_unit  | TRUE ⦄[x::=v]τv = ⦃ z : B_unit  | TRUE ⦄" using subst_tv.simps subst_cv.simps check_assignI by presburger
    ultimately show   "P ; ℬ ; Γ[x::=v]Γv  ⊢ ⦃ z : B_unit  | TRUE ⦄ ≲ τ'[x::=v]τv" using gs by auto
  qed
  thus ?case using subst_sv.simps(5) by auto

next
  case (check_whileI Θ Φ ℬ Γ Δ s1 z' s2 τ')
  have " wfG Θ ℬ (Γ2 @ (x, b, c[z::=[x]v]cv) #Γ Γ1)" using check_whileI check_s_wf by meson
  hence **: " Γ[x::=v]Γv = Γ2[x::=v]Γv@Γ1" using subst_g_inside wf check_whileI  by auto
  have teq: "(⦃ z : B_unit  | TRUE ⦄)[x::=v]τv = (⦃ z : B_unit  | TRUE ⦄)"  by(auto simp add: subst_sv.simps check_whileI)
  moreover have "(⦃ z : B_unit  | TRUE ⦄) = (⦃ z' : B_unit  | TRUE ⦄)" using type_eq_flip c.fresh flip_fresh_fresh by metis
  ultimately have  teq2:"(⦃ z' : B_unit  | TRUE ⦄)[x::=v]τv = (⦃ z' : B_unit  | TRUE ⦄)" by metis

  hence "Θ ; Φ ; ℬ ; Γ[x::=v]Γv ; Δ[x::=v]Δv  ⊢ s1[x::=v]sv ⇐ ⦃ z' : B_bool  | TRUE ⦄" using check_whileI  subst_sv.simps subst_top_eq by metis
  moreover have "Θ ; Φ ; ℬ ; Γ[x::=v]Γv ; Δ[x::=v]Δv  ⊢ s2[x::=v]sv ⇐ ⦃ z' : B_unit  | TRUE ⦄" using check_whileI subst_top_eq by metis
  moreover have "Θ ; ℬ ; Γ[x::=v]Γv  ⊢ ⦃ z' : B_unit  | TRUE ⦄ ≲ τ'[x::=v]τv" proof -
    have "Θ ; ℬ ; Γ2[x::=v]Γv @ Γ1  ⊢ ⦃ z' : B_unit  | TRUE ⦄[x::=v]τv ≲ τ'[x::=v]τv" proof(rule subst_subtype_tau)
      show "Θ ; ℬ ; Γ1  ⊢ v ⇒ τ" by(auto simp add: check_whileI)
      show "Θ ; ℬ ; Γ1  ⊢ τ ≲ ⦃ z : b  | c ⦄"  by(auto simp add: check_whileI)
      show "Θ ; ℬ ; Γ2 @ (x, b, c[z::=[x]v]cv) #Γ Γ1  ⊢ ⦃ z' : B_unit  | TRUE ⦄ ≲ τ'"  using check_whileI by metis
      show "atom z ♯ (x, v)" by(auto simp add: check_whileI)
    qed
    thus ?thesis using teq2 ** by auto
  qed

  ultimately have  " Θ ; Φ ; ℬ ; Γ[x::=v]Γv ; Δ[x::=v]Δv  ⊢ AS_while s1[x::=v]sv s2[x::=v]sv ⇐ τ'[x::=v]τv" 
    using Typing.check_whileI  by metis
  then show ?case  using subst_sv.simps by metis
next
  case (check_seqI P Φ ℬ Γ Δ   s1 z s2 τ ) 
  hence "P ; Φ; ℬ ; Γ[x::=v]Γv ;  Δ[x::=v]Δv   ⊢ AS_seq (s1[x::=v]sv) (s2[x::=v]sv)  ⇐ τ[x::=v]τv" using Typing.check_seqI subst_top_eq check_seqI by metis
  then show ?case using subst_sv.simps by metis
next
  case (check_caseI Θ Φ ℬ Γ Δ tid dclist v' cs τ  za)

  have wf: "wfG Θ ℬ Γ" using check_caseI  check_v_wf  by simp
  have **: "Γ[x::=v]Γv = Γ2[x::=v]Γv@Γ1" using subst_g_inside wf check_caseI by auto

  have "Θ ; Φ ; ℬ ; Γ[x::=v]Γv ; Δ[x::=v]Δv  ⊢ AS_match (v'[x::=v]vv) (subst_branchlv cs x v) ⇐ τ[x::=v]τv" proof(rule  Typing.check_caseI )
    show "check_branch_list Θ Φ ℬ (Γ[x::=v]Γv) Δ[x::=v]Δv tid dclist v'[x::=v]vv (subst_branchlv cs x v ) (τ[x::=v]τv)"  using check_caseI by auto
    show "AF_typedef tid dclist ∈ set Θ" using check_caseI by auto
    show "Θ ; ℬ ; Γ[x::=v]Γv  ⊢ v'[x::=v]vv ⇐ ⦃ za : B_id tid  | TRUE ⦄" proof -
      have "Θ ; ℬ ; Γ2 @ (x, b, c[z::=[x]v]cv) #Γ Γ1  ⊢ v' ⇐  ⦃ za : B_id tid  | TRUE ⦄"
        using check_caseI by argo
      hence "Θ ; ℬ ; Γ2[x::=v]Γv @ Γ1  ⊢ v'[x::=v]vv ⇐  (⦃ za : B_id tid  | TRUE ⦄)[x::=v]τv" 
        using check_caseI subst_infer_check_v[OF check_caseI(7) _  check_caseI(8)  check_caseI(9)] by meson
      moreover have "(⦃ za : B_id tid  | TRUE ⦄) = ((⦃ za : B_id tid  | TRUE ⦄)[x::=v]τv)"  
        using subst_cv.simps subst_tv.simps subst_cv_true by fast
      ultimately show  ?thesis using check_caseI ** by argo
    qed
    show "wfTh Θ" using check_caseI by auto
  qed
  thus ?case using subst_branchlv.simps subst_sv.simps(4) by metis
next
  case (check_ifI z' Θ Φ ℬ Γ Δ va s1 s2 τ')
  show ?case unfolding  subst_sv.simps proof
    show ‹atom z' ♯ (Θ, Φ, ℬ, Γ[x::=v]Γv, Δ[x::=v]Δv, va[x::=v]vv, s1[x::=v]sv, s2[x::=v]sv, τ'[x::=v]τv)› 
      by(subst_tuple_mth add: check_ifI)    
    have *:"⦃ z' : B_bool  | TRUE ⦄[x::=v]τv = ⦃ z' : B_bool  | TRUE ⦄" using subst_tv.simps check_ifI 
      by (metis freshers(19) subst_cv.simps(1) type_eq_subst)
    have **: "Γ[x::=v]Γv = Γ2[x::=v]Γv@Γ1" using subst_g_inside wf check_ifI check_v_wf by metis
    show   ‹Θ ; ℬ ; Γ[x::=v]Γv  ⊢ va[x::=v]vv ⇐ ⦃ z' : B_bool  | TRUE ⦄› 
    proof(subst *[symmetric], rule subst_infer_check_v1[where Γ1=Γ2 and Γ2=Γ1])
      show "Γ = Γ2 @ ((x, b ,c[z::=[ x ]v]cv) #Γ Γ1)" using check_ifI by metis
      show ‹ Θ ; ℬ ; Γ1 ⊢ v ⇒ τ› using check_ifI by metis
      show ‹Θ ; ℬ ; Γ  ⊢ va ⇐ ⦃ z' : B_bool  | TRUE ⦄› using check_ifI by metis
      show ‹Θ ; ℬ ; Γ1  ⊢ τ ≲ ⦃ z : b  | c ⦄› using check_ifI by metis
      show ‹atom z ♯ (x, v)› using check_ifI by metis
    qed

    have " ⦃ z' : b_of τ'[x::=v]τv  | [ va[x::=v]vv ]ce  ==  [ [ L_true ]v ]ce   IMP  c_of τ'[x::=v]τv z'  ⦄ = ⦃ z' : b_of τ'  | [ va ]ce  ==  [ [ L_true ]v ]ce   IMP  c_of τ' z'  ⦄[x::=v]τv"
      by(simp add: subst_tv.simps fresh_Pair check_ifI b_of_subst subst_v_c_of)

    thus  ‹ Θ ; Φ ; ℬ ; Γ[x::=v]Γv ; Δ[x::=v]Δv  ⊢ s1[x::=v]sv ⇐ ⦃ z' : b_of τ'[x::=v]τv  | [ va[x::=v]vv ]ce  ==  [ [ L_true ]v ]ce   IMP  c_of τ'[x::=v]τv z'  ⦄›      
      using check_ifI by metis
    have " ⦃ z' : b_of τ'[x::=v]τv  | [ va[x::=v]vv ]ce  ==  [ [ L_false ]v ]ce   IMP  c_of τ'[x::=v]τv z'  ⦄ = ⦃ z' : b_of τ'  | [ va ]ce  ==  [ [ L_false ]v ]ce   IMP  c_of τ' z'  ⦄[x::=v]τv"
      by(simp add: subst_tv.simps fresh_Pair check_ifI b_of_subst subst_v_c_of)
    thus ‹ Θ ; Φ ; ℬ ; Γ[x::=v]Γv ; Δ[x::=v]Δv  ⊢ s2[x::=v]sv ⇐ ⦃ z' : b_of τ'[x::=v]τv  | [ va[x::=v]vv ]ce  ==  [ [ L_false ]v ]ce   IMP  c_of τ'[x::=v]τv z'  ⦄› 
      using check_ifI by metis
  qed
qed

lemma subst_check_check_s:
  fixes v::v and s::s and cs::branch_s and x::x and c::c and b::b and Γ1::Γ and Γ2::Γ
  assumes "Θ ; ℬ ; Γ1 ⊢ v ⇐ ⦃ z : b | c ⦄"  and  "atom z ♯ (x, v)"
    and  "check_s Θ Φ ℬ Γ Δ  s  τ'" and "Γ  = (Γ2@((x,b,c[z::=[x]v]cv)#ΓΓ1))" 
  shows "check_s Θ Φ ℬ (subst_gv Γ x v)    Δ[x::=v]Δv  (s[x::=v]sv)  (subst_tv  τ' x v )" 
proof -
  obtain τ where  "Θ ; ℬ ; Γ1 ⊢ v ⇒ τ ∧ Θ ; ℬ ; Γ1 ⊢ τ ≲ ⦃ z : b | c ⦄" using check_v_elims assms by auto
  thus ?thesis using subst_infer_check_s assms by metis
qed

text ‹ If a statement checks against a type @{text "τ"} then it checks against a supertype of @{text "τ"} ›
lemma check_s_supertype:
  fixes v::v and s::s and cs::branch_s and x::x and c::c and b::b and Γ::Γ and Γ'::Γ and css::branch_list
  shows  "check_s Θ Φ ℬ G Δ  s  t1 ⟹ Θ ; ℬ ; G ⊢ t1 ≲ t2  ⟹ check_s Θ Φ ℬ G Δ  s  t2"  and 
    "check_branch_s Θ Φ ℬ G Δ tid cons const v cs t1 ⟹ Θ ; ℬ ; G ⊢ t1 ≲ t2 ⟹ check_branch_s Θ Φ ℬ G Δ tid cons const v cs t2" and
    "check_branch_list Θ Φ ℬ G Δ tid dclist v css t1 ⟹ Θ ; ℬ ; G ⊢ t1 ≲ t2 ⟹ check_branch_list Θ Φ ℬ G Δ tid dclist v css t2"
proof(induct arbitrary: t2 and t2 and t2 rule: check_s_check_branch_s_check_branch_list.inducts)
  case (check_valI  Θ ℬ Γ Δ  Φ v τ' τ  )
  hence " Θ ; ℬ ; Γ ⊢ τ' ≲ t2" using subtype_trans by meson
  then show ?case using subtype_trans Typing.check_valI check_valI by metis

next
  case (check_letI x Θ Φ ℬ Γ Δ e τ z s b c)
  show ?case proof(rule Typing.check_letI)
    show "atom x ♯(Θ, Φ, ℬ, Γ, Δ, e, t2)" using check_letI subtype_fresh_tau fresh_prodN by metis
    show "atom z ♯ (x, Θ, Φ, ℬ, Γ, Δ, e, t2, s)" using check_letI(2) subtype_fresh_tau[of z τ Γ _ _ t2] fresh_prodN check_letI(6) by auto
    show "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ e ⇒ ⦃ z : b  | c ⦄" using check_letI by meson

    have "wfG Θ ℬ ((x, b, c[z::=[x]v]v) #Γ Γ)" using check_letI check_s_wf subst_defs by metis
    moreover have "toSet Γ ⊆ toSet ((x, b, c[z::=[x]v]v) #Γ Γ)" by auto
    ultimately have "  Θ ; ℬ ; (x, b, c[z::=[x]v]v) #Γ Γ  ⊢ τ ≲ t2" using subtype_weakening[OF check_letI(6)] by auto
    thus  "Θ ; Φ ; ℬ ; (x, b, c[z::=[x]v]v) #Γ Γ ; Δ  ⊢ s ⇐ t2" using check_letI subst_defs by metis
  qed
next  
  case (check_branch_list_consI Θ Φ ℬ Γ Δ tid dclist v cs τ css)
  then show ?case using  Typing.check_branch_list_consI by auto
next
  case (check_branch_list_finalI Θ Φ ℬ Γ Δ tid dclist v cs τ)
  then show ?case using  Typing.check_branch_list_finalI by auto
next
  case (check_branch_s_branchI Θ ℬ Γ Δ τ const x Φ tid cons v s)
  show  ?case proof
    have "atom x ♯ t2" using subtype_fresh_tau[of x τ ] check_branch_s_branchI(5,8)   fresh_prodN by metis
    thus  "atom x ♯ (Θ, Φ, ℬ, Γ, Δ, tid, cons, const, v, t2)" using check_branch_s_branchI  fresh_prodN by metis
    show  "wfT Θ ℬ Γ t2" using subtype_wf check_branch_s_branchI by meson
    show  "Θ ; Φ ; ℬ ; (x, b_of const, CE_val v  ==  CE_val(V_cons tid cons (V_var x)) AND c_of const x) #Γ Γ ; Δ  ⊢ s ⇐ t2" proof -
      have "wfG Θ ℬ ((x, b_of const, CE_val v  ==  CE_val(V_cons tid cons (V_var x))   AND c_of const x) #Γ Γ)" using check_s_wf check_branch_s_branchI by metis
      moreover have "toSet Γ ⊆ toSet ((x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x)) AND c_of const x) #Γ Γ)" by auto
      hence "Θ ; ℬ ; ((x, b_of const, CE_val v  ==  CE_val(V_cons tid cons (V_var x)) AND c_of const x) #Γ Γ) ⊢ τ ≲ t2" 
        using check_branch_s_branchI subtype_weakening 
        using calculation by presburger
      thus ?thesis using check_branch_s_branchI by presburger
    qed
  qed(auto simp add: check_branch_s_branchI)
next
  case (check_ifI z Θ Φ ℬ Γ Δ v s1 s2 τ)
  show  ?case proof(rule Typing.check_ifI)
    have *:"atom z ♯ t2" using subtype_fresh_tau[of z τ Γ ] check_ifI   fresh_prodN by auto
    thus ‹atom z ♯ (Θ, Φ, ℬ, Γ, Δ, v, s1, s2, t2)› using check_ifI fresh_prodN by auto
    show ‹Θ ; ℬ ; Γ  ⊢ v ⇐ ⦃ z : B_bool  | TRUE ⦄› using check_ifI by auto
    show ‹ Θ ; Φ ; ℬ ; Γ ; Δ  ⊢ s1 ⇐ ⦃ z : b_of t2  | [ v ]ce  ==  [ [ L_true ]v ]ce   IMP  c_of t2 z  ⦄› 
      using check_ifI subtype_if1 fresh_prodN base_for_lit.simps b_of.simps * check_v_wf by metis

    show ‹ Θ ; Φ ; ℬ ; Γ ; Δ  ⊢ s2 ⇐ ⦃ z : b_of t2  | [ v ]ce  ==  [ [ L_false ]v ]ce   IMP  c_of t2 z  ⦄›
      using check_ifI subtype_if1 fresh_prodN base_for_lit.simps b_of.simps * check_v_wf by metis
  qed
next
  case (check_assertI x Θ Φ ℬ Γ Δ c τ s)

  show ?case proof
    have "atom x ♯ t2" using subtype_fresh_tau[OF _ _ ‹Θ ; ℬ ; Γ  ⊢ τ ≲ t2›] check_assertI fresh_prodN by simp
    thus  "atom x ♯ (Θ, Φ, ℬ, Γ, Δ, c, t2, s)"   using subtype_fresh_tau check_assertI   fresh_prodN by simp
    have "Θ ; ℬ ; (x, B_bool, c) #Γ Γ  ⊢ τ ≲ t2" apply(rule subtype_weakening) 
      using check_assertI apply simp
      using toSet.simps apply blast
      using check_assertI check_s_wf by simp
    thus  "Θ ; Φ ; ℬ ; (x, B_bool, c) #Γ Γ ; Δ  ⊢ s ⇐ t2" using check_assertI by simp
    show "Θ ; ℬ ; Γ  ⊨ c " using check_assertI by auto
    show "Θ ; ℬ ; Γ ⊢wf Δ " using check_assertI by auto
  qed
next
  case (check_let2I x P Φ ℬ G Δ t s1 τ s2 )
  have "wfG P ℬ ((x, b_of t, c_of t x) #Γ G)" 
    using check_let2I check_s_wf by metis
  moreover have "toSet G ⊆ toSet ((x, b_of t, c_of t x) #Γ G)" by auto
  ultimately have  *:"P ; ℬ ; (x, b_of t, c_of t x) #Γ G  ⊢ τ ≲ t2" using check_let2I subtype_weakening by metis
  show  ?case proof(rule Typing.check_let2I)
    have "atom x ♯ t2" using subtype_fresh_tau[of x τ ] check_let2I   fresh_prodN by metis  
    thus "atom x ♯ (P, Φ, ℬ, G, Δ, t, s1, t2)" using check_let2I  fresh_prodN by metis
    show "P ; Φ ; ℬ ; G ; Δ  ⊢ s1 ⇐ t"  using check_let2I by blast
    show "P ; Φ ; ℬ ;(x, b_of t, c_of t x ) #Γ G ; Δ  ⊢ s2 ⇐ t2" using check_let2I * by blast
  qed
next
  case (check_varI u Θ Φ ℬ Γ Δ τ' v τ s)
  show ?case proof(rule Typing.check_varI)
    have "atom u ♯ t2" using u_fresh_t by auto
    thus ‹atom u ♯ (Θ, Φ, ℬ, Γ, Δ, τ', v, t2)› using check_varI  fresh_prodN by auto
    show ‹Θ ; ℬ ; Γ  ⊢ v ⇐ τ'› using check_varI by auto
    show ‹ Θ ; Φ ; ℬ ; Γ ; (u, τ') #Δ Δ  ⊢ s ⇐ t2› using check_varI by auto
  qed
next
  case (check_assignI Δ u τ P G v z τ')
  then show ?case using Typing.check_assignI by (meson subtype_trans)
next
  case (check_whileI Δ G P s1 z s2 τ')
  then show ?case using Typing.check_whileI by (meson subtype_trans)
next
  case (check_seqI Δ G P s1 z s2 τ)
  then show ?case using Typing.check_seqI by blast
next
  case (check_caseI Δ Γ Θ tid cs τ v z)
  then show ?case using Typing.check_caseI subtype_trans   by meson

qed

lemma subtype_let:
  fixes s'::s and cs::branch_s and css::branch_list and v::v
  shows "Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AS_let x e1 s ⇐ τ ⟹ Θ ; Φ ; ℬ ; GNil ; Δ  ⊢ e1 ⇒ τ1 ⟹ 
        Θ ; Φ ; ℬ ; GNil ; Δ  ⊢ e2 ⇒ τ2 ⟹ Θ ; ℬ ; GNil ⊢ τ2 ≲ τ1 ⟹ Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AS_let x e2 s ⇐ τ" and
    "check_branch_s Θ Φ  {||} GNil Δ tid dc const v cs τ ⟹ True" and 
    "check_branch_list Θ Φ  {||} Γ Δ tid dclist v css τ ⟹ True"
proof(nominal_induct GNil  Δ "AS_let x e1 s" τ and τ and τ avoiding: e2  τ1 τ2 
    rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_letI x1 Θ Φ ℬ  Δ τ1 z1 s1 b1 c1)
  obtain z2 and b2 and c2 where t2:"τ2 = ⦃ z2 : b2 | c2 ⦄ ∧ atom z2 ♯ (x1, Θ, Φ, ℬ, GNil, Δ, e2, τ1, s1) " 
    using obtain_fresh_z by metis

  obtain z1a and b1a and c1a where t1:"τ1 = ⦃ z1a : b1a  | c1a ⦄ ∧ atom z1a ♯ x1" using infer_e_uniqueness check_letI by  metis
  hence t3: " ⦃ z1a : b1a  | c1a ⦄  =  ⦃ z1 : b1  | c1 ⦄ " using infer_e_uniqueness check_letI by  metis 

  have beq: "b1a = b2 ∧ b2 = b1" using check_letI subtype_eq_base t1 t2 t3 by metis

  have " Θ ; Φ ; ℬ ; GNil ; Δ   ⊢ AS_let x1  e2 s1 ⇐ τ1"  proof
    show ‹atom x1 ♯ (Θ, Φ, ℬ, GNil, Δ, e2, τ1)› using check_letI t2 fresh_prodN by metis
    show ‹atom z2 ♯ (x1, Θ, Φ, ℬ, GNil, Δ, e2, τ1, s1)› using check_letI t2  using check_letI t2 fresh_prodN by metis
    show ‹Θ ; Φ ; ℬ ; GNil ; Δ  ⊢ e2 ⇒ ⦃ z2 : b2  | c2 ⦄› using check_letI t2 by metis

    have ‹ Θ ; Φ ; ℬ ; GNil@(x1, b2, c2[z2::=[ x1 ]v]cv) #Γ GNil ; Δ  ⊢ s1 ⇐ τ1›
    proof(rule ctx_subtype_s)
      have "c1a[z1a::=[ x1 ]v]cv = c1[z1::=[ x1 ]v]cv" using subst_v_flip_eq_two subst_v_c_def t3 τ.eq_iff by metis
      thus  ‹ Θ ; Φ ; ℬ ; GNil @ (x1, b2, c1a[z1a::=[ x1 ]v]cv) #Γ GNil ; Δ  ⊢ s1 ⇐ τ1› using check_letI beq append_g.simps subst_defs by metis
      show ‹Θ ; ℬ ; GNil  ⊢ ⦃ z2 : b2  | c2 ⦄ ≲ ⦃ z1a : b2  | c1a ⦄› using check_letI beq  t1 t2 by metis
      have "atom x1 ♯ c2" using t2 check_letI τ_fresh_c fresh_prodN  by blast
      moreover have "atom x1 ♯ c1a" using t1 check_letI τ_fresh_c fresh_prodN  by blast
      ultimately show ‹atom x1 ♯ (z1a, z2, c1a, c2)› using t1 t2 fresh_prodN fresh_x_neq by metis
    qed

    thus ‹ Θ ; Φ ; ℬ ; (x1, b2, c2[z2::=[ x1 ]v]v) #Γ GNil ; Δ  ⊢ s1 ⇐ τ1› using append_g.simps subst_defs by metis
  qed

  moreover have "AS_let x1  e2 s1 = AS_let x  e2 s" using check_letI s_branch_s_branch_list.eq_iff  by metis

  ultimately show ?case  by metis

qed(auto+)

end