Theory Safety

(*<*)
theory Safety
  imports Operational IVSubstTypingL BTVSubstTypingL 
begin
  (*>*)

method supp_calc = (metis (mono_tags, opaque_lifting) pure_supp  c.supp e.supp v.supp supp_l_empty opp.supp sup_bot.right_neutral supp_at_base)
declare infer_e.intros[simp]
declare infer_e.intros[intro]

chapter ‹Safety›

text ‹Lemmas about the operational semantics leading up to progress and preservation and then
safety.›

section ‹Store Lemmas›

abbreviation delta_ext (" _ ⊑ _ ") where  
  "delta_ext Δ Δ' ≡ (setD Δ ⊆ setD Δ')" 

nominal_function dc_of :: "branch_s ⇒ string" where
  "dc_of (AS_branch dc _ _) = dc"
  apply(auto,simp add: eqvt_def dc_of_graph_aux_def)
  using   s_branch_s_branch_list.exhaust by metis
nominal_termination (eqvt) by lexicographic_order

lemma delta_sim_fresh: 
  assumes "Θ ⊢ δ ∼ Δ" and "atom u ♯ δ"
  shows "atom u ♯ Δ"
  using assms proof(induct rule : delta_sim.inducts)
  case (delta_sim_nilI Θ)
  then show ?case using fresh_def supp_DNil by blast
next
  case (delta_sim_consI Θ δ Δ v τ u')
  hence  "Θ ; {||} ; GNil ⊢wf τ" using check_v_wf  by meson
  hence  "supp τ = {}" using  wfT_supp by fastforce
  moreover have  "atom u ♯ u'" using delta_sim_consI fresh_Cons fresh_Pair by blast
  moreover have "atom u ♯ Δ" using delta_sim_consI fresh_Cons by blast
  ultimately show ?case using fresh_Pair fresh_DCons fresh_def by blast
qed

lemma delta_sim_v: 
  fixes Δ::Δ
  assumes "Θ ⊢ δ ∼ Δ " and "(u,v) ∈ set δ" and "(u,τ) ∈ setD Δ" and "Θ ; {||} ; GNil ⊢wf Δ"
  shows "Θ ; {||} ; GNil ⊢ v ⇐ τ"
  using assms proof(induct δ arbitrary: Δ)
  case Nil
  then show ?case by auto
next
  case (Cons uv δ)
  obtain u' and v' where uv : "uv=(u',v')" by fastforce
  show ?case proof(cases "u'=u")
    case True
    hence  *:"Θ ⊢ ((u,v')#δ) ∼ Δ" using uv Cons by blast
    then obtain τ' and Δ' where tt: "Θ ; {||} ; GNil ⊢ v' ⇐ τ' ∧ u ∉ fst ` set δ ∧ Δ = (u,τ')#ΔΔ'" using delta_sim_elims(3)[OF *] by metis
    moreover hence "v'=v" using Cons True 
      by (metis Pair_inject fst_conv image_eqI set_ConsD uv)
    moreover have "τ=τ'" using wfD_unique tt Cons 
        setD.simps list.set_intros by blast
    ultimately show ?thesis by metis
  next
    case False
    hence  *:"Θ ⊢ ((u',v')#δ) ∼ Δ" using uv Cons by blast
    then obtain τ' and Δ' where tt: "Θ ⊢ δ ∼ Δ' ∧ Θ ; {||} ; GNil ⊢ v' ⇐ τ' ∧ u' ∉ fst ` set δ ∧ Δ = (u',τ')#ΔΔ'" using delta_sim_elims(3)[OF *] by metis

    moreover hence "Θ ; {||} ; GNil ⊢wf Δ'" using wfD_elims Cons delta_sim_elims by metis
    ultimately show ?thesis using Cons  
      using False by auto
  qed
qed

lemma delta_sim_delta_lookup:
  assumes "Θ ⊢ δ ∼ Δ " and "(u, ⦃ z : b  | c ⦄) ∈ setD Δ" 
  shows "∃v. (u,v) ∈ set δ"
  using assms by(induct rule: delta_sim.inducts,auto+)

lemma update_d_stable:
  "fst ` set δ = fst ` set (update_d δ u v)"
proof(induct δ)
  case Nil
  then show ?case by auto
next
  case (Cons a δ)
  then show ?case using update_d.simps
    by (metis (no_types, lifting) eq_fst_iff image_cong image_insert list.simps(15) prod.exhaust_sel)
qed

lemma update_d_sim:
  fixes Δ::Δ
  assumes "Θ ⊢ δ ∼ Δ" and "Θ ; {||} ; GNil ⊢ v ⇐ τ" and "(u,τ) ∈ setD Δ" and "Θ ; {||} ; GNil  ⊢wf Δ"
  shows "Θ ⊢ (update_d δ u v) ∼ Δ"
  using assms proof(induct δ arbitrary: Δ)
  case Nil
  then show ?case using delta_sim_consI by simp
next
  case (Cons uv δ)
  obtain u' and v' where uv : "uv=(u',v')" by fastforce

  hence  *:"Θ ⊢ ((u',v')#δ) ∼ Δ" using uv Cons by blast
  then obtain τ' and Δ' where tt: "Θ ⊢ δ ∼ Δ' ∧ Θ ; {||} ; GNil ⊢ v' ⇐ τ' ∧ u' ∉ fst ` set δ ∧ Δ = (u',τ')#ΔΔ'" using delta_sim_elims * by metis

  show ?case proof(cases "u=u'")
    case True
    then have "(u,τ') ∈ setD Δ" using tt by auto
    then have "τ = τ'" using Cons  wfD_unique by metis
    moreover  have "update_d ((u',v')#δ) u v = ((u',v)#δ)" using update_d.simps True by presburger
    ultimately show ?thesis using delta_sim_consI tt Cons True 
      by (simp add: tt uv)
  next
    case False
    have  "Θ ⊢ (u',v') # (update_d δ u v) ∼ (u',τ')#ΔΔ'" 
    proof(rule delta_sim_consI)
      show "Θ ⊢ update_d δ u v ∼ Δ' " using Cons using delta_sim_consI 
          delta_sim.simps update_d.simps Cons  delta_sim_elims uv  tt 
          False fst_conv set_ConsD wfG_elims wfD_elims  by (metis setD_ConsD)
      show "Θ ; {||} ; GNil  ⊢ v' ⇐ τ'" using tt by auto
      show "u' ∉ fst ` set (update_d δ u v)" using  update_d.simps Cons update_d_stable tt by auto
    qed
    thus  ?thesis using False update_d.simps uv 
      by (simp add: tt)
  qed
qed

section ‹Preservation›
text ‹Types are preserved under reduction step. Broken down into lemmas about different operations›

subsection ‹Function Application›

lemma check_s_x_fresh:
  fixes x::x and s::s
  assumes "Θ ; Φ ; B ;  GNil ; D  ⊢ s ⇐ τ" 
  shows "atom x ♯ s ∧ atom x ♯ τ ∧ atom x ♯ D"
proof - 
  have "Θ ; Φ ; B ; GNil ; D ⊢wf s : b_of τ"  using check_s_wf[OF assms] by auto 
  moreover have "Θ ; B ; GNil   ⊢wf τ " using check_s_wf assms by auto
  moreover have "Θ ; B ; GNil   ⊢wf D" using check_s_wf assms by auto
  ultimately show ?thesis using wf_supp x_fresh_u 
    by (meson fresh_GNil wfS_x_fresh wfT_x_fresh wfD_x_fresh)
qed

lemma check_funtyp_subst_b: 
  fixes b'::b
  assumes "check_funtyp Θ Φ {|bv|} (AF_fun_typ x b c τ s)" and ‹ Θ ; {||}  ⊢wf b' ›
  shows "check_funtyp Θ Φ  {||} (AF_fun_typ x b[bv::=b']bb (c[bv::=b']cb) τ[bv::=b']τb s[bv::=b']sb)"
  using assms proof (nominal_induct "{|bv|}" "AF_fun_typ x b c τ s" rule: check_funtyp.strong_induct)
  case (check_funtypI x' Θ Φ c' s' τ')
  have "check_funtyp Θ Φ {||} (AF_fun_typ x' b[bv::=b']bb (c'[bv::=b']cb) τ'[bv::=b']τb s'[bv::=b']sb)" proof
    show ‹atom x' ♯ (Θ, Φ, {||}::bv fset, b[bv::=b']bb)› using check_funtypI fresh_prodN x_fresh_b fresh_empty_fset by metis

    have  ‹ Θ ; Φ ; {||} ; ((x', b, c') #Γ GNil)[bv::=b']Γb ; []Δ[bv::=b']Δb  ⊢ s'[bv::=b']sb ⇐ τ'[bv::=b']τb›  proof(rule subst_b_check_s)
      show ‹ Θ ; {||}  ⊢wf b' › using check_funtypI by metis
      show ‹{|bv|} = {|bv|}› by auto
      show ‹ Θ ; Φ ; {|bv|} ; (x', b, c') #Γ GNil ; []Δ  ⊢ s' ⇐ τ'› using check_funtypI by metis
    qed

    thus ‹ Θ ; Φ ; {||} ; (x', b[bv::=b']bb, c'[bv::=b']cb) #Γ GNil ; []Δ  ⊢ s'[bv::=b']sb ⇐ τ'[bv::=b']τb› 
      using subst_gb.simps subst_db.simps by simp
  qed

  moreover have "(AF_fun_typ x b c τ s) = (AF_fun_typ x' b c' τ' s')"  using fun_typ.eq_iff check_funtypI by metis
  moreover hence "(AF_fun_typ x b[bv::=b']bb (c[bv::=b']cb) τ[bv::=b']τb s[bv::=b']sb) = (AF_fun_typ x' b[bv::=b']bb (c'[bv::=b']cb) τ'[bv::=b']τb s'[bv::=b']sb)"
    using  subst_ft_b.simps by metis
  ultimately show  ?case by metis
qed

lemma funtyp_simple_check:
  fixes s::s  and Δ::Δ and τ::τ and v::v  
  assumes "check_funtyp Θ Φ  ({||}::bv fset) (AF_fun_typ x b c τ s)" and
    "Θ ; {||} ; GNil ⊢ v ⇐ ⦃ x : b | c ⦄" 
  shows "Θ ; Φ ;  {||} ; GNil ; DNil ⊢ s[x::=v]sv ⇐ τ[x::=v]τv"
  using assms proof(nominal_induct  " ({||}::bv fset)" "AF_fun_typ x b c τ s" avoiding: v x  rule: check_funtyp.strong_induct)
  case (check_funtypI x' Θ Φ c' s' τ')

  hence eq1: "⦃ x' : b  | c' ⦄ = ⦃ x : b  | c ⦄" using funtyp_eq_iff_equalities by metis

  obtain x'' and c'' where xf:"⦃ x : b  | c ⦄ = ⦃ x'' : b | c'' ⦄ ∧ atom x'' ♯ (x',v) ∧ atom x'' ♯ (x,c)" using obtain_fresh_z3 by metis 
  moreover have "atom x' ♯ c''" proof -
    have "supp  ⦃ x'' : b | c'' ⦄ = {}" using eq1 check_funtypI xf check_v_wf wfT_nil_supp by metis 
    hence "supp c'' ⊆ { atom x'' }" using  τ.supp eq1 xf by (auto simp add: freshers)
    moreover have "atom x' ≠ atom x''" using xf fresh_Pair fresh_x_neq by metis
    ultimately show ?thesis using xf fresh_Pair fresh_x_neq fresh_def fresh_at_base by blast
  qed
  ultimately have eq2: "c''[x''::=[ x' ]v]cv = c'" using eq1  type_eq_subst_eq3(1)[of x' b c' x'' b  c''] by metis

  have "atom x' ♯ c" proof -
    have "supp  ⦃ x : b | c ⦄ = {}" using eq1 check_funtypI xf check_v_wf wfT_nil_supp by metis 
    hence "supp c ⊆ { atom x }" using  τ.supp by auto
    moreover have "atom x ≠ atom x'" using check_funtypI fresh_Pair fresh_x_neq by metis
    ultimately show ?thesis using fresh_def by force
  qed
  hence eq: " c[x::=[ x' ]v]cv =  c' ∧ s'[x'::=v]sv = s[x::=v]sv ∧ τ'[x'::=v]τv = τ[x::=v]τv" 
    using funtyp_eq_iff_equalities type_eq_subst_eq3 check_funtypI by metis

  have " Θ ; Φ ; {||} ; ((x', b, c''[x''::=[ x' ]v]cv) #Γ GNil)[x'::=v]Γv ; []Δ[x'::=v]Δv  ⊢ s'[x'::=v]sv ⇐ τ'[x'::=v]τv" 
  proof(rule subst_check_check_s )
    show ‹Θ ; {||} ; GNil  ⊢ v ⇐ ⦃ x'' : b  | c'' ⦄› using check_funtypI eq1 xf by metis
    show ‹atom x'' ♯ (x', v)› using check_funtypI fresh_x_neq fresh_Pair xf by metis
    show ‹ Θ ; Φ ; {||} ; (x', b, c''[x''::=[ x' ]v]cv) #Γ GNil ; []Δ  ⊢ s' ⇐ τ'› using check_funtypI eq2 by metis
    show ‹ (x', b, c''[x''::=[ x' ]v]cv) #Γ GNil = GNil  @ (x', b, c''[x''::=[ x' ]v]cv) #Γ GNil› using append_g.simps by auto
  qed
  hence " Θ; Φ; {||}; GNil; []Δ  ⊢ s'[x'::=v]sv ⇐ τ'[x'::=v]τv" using subst_gv.simps subst_dv.simps by auto
  thus ?case using eq  by auto
qed

lemma funtypq_simple_check:
  fixes s::s  and Δ::Δ and τ::τ and v::v  
  assumes "check_funtypq Θ Φ   (AF_fun_typ_none (AF_fun_typ x b c t s))" and
    "Θ ; {||} ; GNil ⊢ v ⇐ ⦃ x : b | c ⦄" 
  shows "Θ; Φ; {||}; GNil; DNil ⊢ s[x::=v]sv ⇐ t[x::=v]τv"
  using assms proof(nominal_induct  "(AF_fun_typ_none (AF_fun_typ x b c t s))" avoiding: v rule: check_funtypq.strong_induct)
  case (check_fundefq_simpleI Θ Φ x' c' t' s')
  hence eq: "⦃ x : b  | c ⦄ = ⦃ x' : b  | c' ⦄ ∧ s'[x'::=v]sv = s[x::=v]sv ∧ t[x::=v]τv = t'[x'::=v]τv" 
    using funtyp_eq_iff_equalities by metis
  hence "Θ; Φ; {||}; GNil; []Δ  ⊢ s'[x'::=v]sv ⇐ t'[x'::=v]τv" 
    using funtyp_simple_check[OF check_fundefq_simpleI(1)] check_fundefq_simpleI by metis
  thus ?case  using eq by metis
qed

lemma funtyp_poly_eq_iff_equalities:
  assumes "[[atom bv']]lst. AF_fun_typ x' b'' c' t' s' = [[atom bv]]lst. AF_fun_typ x b c t s" 
  shows "⦃ x' : b''[bv'::=b']bb  | c'[bv'::=b']cb ⦄ = ⦃ x : b[bv::=b']bb  | c[bv::=b']cb ⦄ ∧ 
          s'[bv'::=b']sb[x'::=v]sv = s[bv::=b']sb[x::=v]sv ∧ t'[bv'::=b']τb[x'::=v]τv = t[bv::=b']τb[x::=v]τv" 
proof - 
  have "subst_ft_b (AF_fun_typ x' b'' c' t' s') bv' b' = subst_ft_b (AF_fun_typ x b c t s) bv b'"
    using subst_b_flip_eq_two subst_b_fun_typ_def assms by metis
  thus ?thesis using fun_typ.eq_iff subst_ft_b.simps funtyp_eq_iff_equalities subst_tb.simps 
    by (metis (full_types) assms fun_poly_arg_unique)

qed

lemma funtypq_poly_check:
  fixes s::s  and Δ::Δ and τ::τ and v::v  and b'::b
  assumes "check_funtypq Θ Φ   (AF_fun_typ_some bv (AF_fun_typ x b c t s))" and
    "Θ ; {||} ; GNil ⊢ v ⇐ ⦃ x : b[bv::=b']bb | c[bv::=b']cb ⦄"   and
    "Θ ; {||} ⊢wf b'" 
  shows "Θ; Φ; {||}; GNil; DNil ⊢ s[bv::=b']sb[x::=v]sv ⇐ t[bv::=b']τb[x::=v]τv"
  using assms proof(nominal_induct  "(AF_fun_typ_some bv (AF_fun_typ x b c t s))" avoiding: v rule: check_funtypq.strong_induct)
  case (check_funtypq_polyI bv' Θ Φ  x' b'' c' t' s')

  hence **:"⦃ x' : b''[bv'::=b']bb  | c'[bv'::=b']cb ⦄ = ⦃ x : b[bv::=b']bb  | c[bv::=b']cb ⦄ ∧ 
          s'[bv'::=b']sb[x'::=v]sv = s[bv::=b']sb[x::=v]sv ∧ t'[bv'::=b']τb[x'::=v]τv = t[bv::=b']τb[x::=v]τv" 
    using funtyp_poly_eq_iff_equalities by metis

  have *:"check_funtyp Θ Φ {||} (AF_fun_typ x' b''[bv'::=b']bb (c'[bv'::=b']cb) (t'[bv'::=b']τb) s'[bv'::=b']sb)"
    using check_funtyp_subst_b[OF check_funtypq_polyI(5) check_funtypq_polyI(8)]  by metis
  moreover have "Θ ; {||} ; GNil  ⊢ v ⇐ ⦃ x' : b''[bv'::=b']bb  | c'[bv'::=b']cb ⦄" using ** check_funtypq_polyI by metis
  ultimately have "Θ; Φ; {||}; GNil; []Δ  ⊢ s'[bv'::=b']sb[x'::=v]sv ⇐ t'[bv'::=b']τb[x'::=v]τv"
    using funtyp_simple_check[OF *] check_funtypq_polyI by metis
  thus ?case using ** by metis

qed

lemma fundef_simple_check:
  fixes s::s  and Δ::Δ and τ::τ and v::v  
  assumes "check_fundef Θ Φ   (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c t s)))" and
    "Θ ; {||} ; GNil ⊢ v ⇐ ⦃ x : b | c ⦄" and "Θ ; {||} ; GNil ⊢wf Δ"
  shows "Θ; Φ; {||}; GNil; Δ ⊢ s[x::=v]sv ⇐ t[x::=v]τv"
  using assms proof(nominal_induct  "(AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c t s)))" avoiding: v rule: check_fundef.strong_induct)
  case (check_fundefI Θ Φ)
  then show ?case using funtypq_simple_check[THEN check_s_d_weakening(1) ] setD.simps by auto
qed

lemma fundef_poly_check:
  fixes s::s  and Δ::Δ and τ::τ and v::v  and b'::b
  assumes "check_fundef Θ Φ   (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c t s)))" and
    "Θ ; {||} ; GNil ⊢ v ⇐ ⦃ x : b[bv::=b']bb | c[bv::=b']cb ⦄" and "Θ ; {||} ; GNil ⊢wf Δ" and  "Θ ; {||} ⊢wf b'" 
  shows "Θ; Φ; {||}; GNil; Δ ⊢ s[bv::=b']sb[x::=v]sv ⇐ t[bv::=b']τb[x::=v]τv" 
  using assms proof(nominal_induct  "(AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c t s)))" avoiding: v rule: check_fundef.strong_induct)
  case (check_fundefI Θ Φ)
  then show ?case using funtypq_poly_check[THEN check_s_d_weakening(1) ] setD.simps by auto
qed

lemma preservation_app:
  assumes
    "Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x1 b1 c1 τ1' s1'))) = lookup_fun Φ f" and  "(∀fd∈set Φ. check_fundef Θ Φ fd)"
  shows "Θ ; Φ ; B ; G ; Δ  ⊢ ss ⇐ τ ⟹  B = {||} ⟹ G = GNil ⟹ ss = LET x = (AE_app f v) IN s ⟹  
           Θ; Φ; {||}; GNil; Δ  ⊢ LET x : (τ1'[x1::=v]τv) = (s1'[x1::=v]sv) IN s ⇐ τ" and
    "check_branch_s Θ Φ ℬ GNil Δ tid dc const v cs τ ⟹ True" and 
    "check_branch_list Θ Φ ℬ Γ Δ tid dclist v css τ ⟹ True"
  using assms proof(nominal_induct τ and τ and τ   avoiding: v rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_letI x2 Θ Φ ℬ Γ Δ e τ z s2 b c)

  hence eq: "e = (AE_app f v)" by simp
  hence *:"Θ ; Φ ; {||} ;GNil ; Δ  ⊢ (AE_app f v) ⇒ ⦃ z : b  | c ⦄" using check_letI by auto

  then obtain x3 b3 c3 τ3 s3 where
    **:"Θ ; {||} ; GNil ⊢wf Δ  ∧  Θ  ⊢wf Φ ∧  Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x3 b3 c3 τ3 s3))) = lookup_fun Φ f ∧ 
     Θ ; {||} ; GNil  ⊢ v ⇐ ⦃ x3 : b3  | c3 ⦄ ∧  atom x3 ♯ (Θ, Φ, ({||}::bv fset), GNil, Δ, v, ⦃ z : b  | c ⦄) ∧  τ3[x3::=v]τv = ⦃ z : b  | c ⦄"
    using infer_e_elims(6)[OF *] subst_defs by metis

  obtain z3 where z3:"⦃ x3 : b3  | c3 ⦄ =  ⦃ z3 : b3  | c3[x3::=V_var z3]cv ⦄ ∧  atom z3 ♯ (x3, v,c3,x1,c1)" using obtain_fresh_z3 by metis

  have seq:"[[atom x3]]lst. s3 = [[atom x1]]lst. s1'" using fun_def_eq check_letI ** option.inject by metis

  let ?ft = "AF_fun_typ x3 b3 c3 τ3 s3"


  have sup: "supp τ3 ⊆ { atom x3} ∧ supp s3 ⊆ { atom x3}"  using wfPhi_f_supp ** by metis

  have "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let2 x2  τ3[x3::=v]τv (s3[x3::=v]sv) s2 ⇐ τ" proof
    show ‹atom x2 ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, τ3[x3::=v]τv, s3[x3::=v]sv, τ)›
      unfolding fresh_prodN using check_letI fresh_subst_v_if subst_v_τ_def sup
      by (metis all_not_in_conv fresh_def fresh_empty_fset fresh_subst_sv_if fresh_subst_tv_if singleton_iff subset_singleton_iff)

    show ‹ Θ; Φ; {||}; GNil; Δ  ⊢ s3[x3::=v]sv ⇐ τ3[x3::=v]τv› proof(rule fundef_simple_check)
      show ‹check_fundef Θ Φ (AF_fundef f (AF_fun_typ_none (AF_fun_typ x3 b3 c3 τ3 s3)))› using ** check_letI lookup_fun_member by metis
      show ‹Θ ; {||} ; GNil  ⊢ v ⇐ ⦃ x3 : b3  | c3 ⦄› using ** by auto
      show ‹ Θ ; {||} ; GNil ⊢wf Δ › using ** by auto
    qed
    show ‹ Θ ; Φ ; {||} ; (x2, b_of τ3[x3::=v]τv, c_of τ3[x3::=v]τv x2) #Γ GNil ; Δ  ⊢ s2 ⇐ τ›  
      using check_letI ** b_of.simps c_of.simps subst_defs  by metis
  qed

  moreover have "AS_let2 x2  τ3[x3::=v]τv (s3[x3::=v]sv) s2 = AS_let2 x   (τ1'[x1::=v]τv) (s1'[x1::=v]sv) s" proof -
    have *: "[[atom x2]]lst. s2 = [[atom x]]lst. s" using check_letI  s_branch_s_branch_list.eq_iff by auto
    moreover have " τ3[x3::=v]τv = τ1'[x1::=v]τv" using fun_ret_unique ** check_letI by metis
    moreover have "s3[x3::=v]sv = (s1'[x1::=v]sv)" using subst_v_flip_eq_two subst_v_s_def seq by metis
    ultimately show ?thesis using s_branch_s_branch_list.eq_iff by metis
  qed

  ultimately show ?case using check_letI by auto
qed(auto+)

lemma fresh_subst_v_subst_b:
  fixes x2::x and tm::"'a::{has_subst_v,has_subst_b}" and x::x
  assumes  "supp tm ⊆ { atom bv, atom x }" and "atom x2 ♯ v" 
  shows  "atom x2 ♯ tm[bv::=b]b[x::=v]v"  
  using assms proof(cases "x2=x")
  case True
  then show ?thesis using fresh_subst_v_if assms by blast
next
  case False
  hence "atom x2 ♯ tm" using assms fresh_def fresh_at_base by force
  hence "atom x2 ♯ tm[bv::=b]b" using  assms fresh_subst_if x_fresh_b False by force
  then show ?thesis using fresh_subst_v_if assms by auto
qed

lemma preservation_poly_app:
  assumes
    "Some (AF_fundef f (AF_fun_typ_some bv1 (AF_fun_typ x1 b1 c1 τ1' s1'))) = lookup_fun Φ f" and  "(∀fd∈set Φ. check_fundef Θ Φ fd)"
  shows "Θ ; Φ ; B ; G ; Δ  ⊢ ss ⇐ τ ⟹  B = {||} ⟹ G = GNil ⟹ ss = LET x = (AE_appP f b' v) IN s ⟹ Θ ; {||}  ⊢wf b'  ⟹ 
               Θ; Φ; {||}; GNil; Δ  ⊢ LET x : (τ1'[bv1::=b']τb[x1::=v]τv) = (s1'[bv1::=b']sb[x1::=v]sv) IN s ⇐ τ" and
    "check_branch_s Θ Φ ℬ GNil Δ tid dc const v cs τ ⟹ True" and 
    "check_branch_list Θ Φ ℬ Γ Δ tid dclist v css τ ⟹ True"
  using assms proof(nominal_induct τ and τ and τ   avoiding: v x1 rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_letI x2 Θ Φ ℬ Γ Δ e τ z s2 b c)

  hence eq: "e = (AE_appP f b' v)" by simp
  hence *:"Θ ; Φ ; {||} ;GNil ; Δ  ⊢ (AE_appP f b' v) ⇒ ⦃ z : b  | c ⦄" using check_letI by auto

  then obtain x3 b3 c3 τ3 s3 bv3 where
    **:"Θ ; {||} ; GNil ⊢wf Δ  ∧  Θ  ⊢wf Φ ∧  Some (AF_fundef f (AF_fun_typ_some bv3 (AF_fun_typ x3 b3 c3 τ3 s3))) = lookup_fun Φ f ∧ 
     Θ ; {||} ; GNil  ⊢ v ⇐ ⦃ x3 : b3[bv3::=b']bb   | c3[bv3::=b']cb  ⦄ ∧  atom x3 ♯ GNil ∧  τ3[bv3::=b']τb[x3::=v]τv = ⦃ z : b  | c ⦄
  ∧ Θ ; {||}  ⊢wf b'"
    using infer_e_elims(21)[OF *] subst_defs  by metis

  obtain z3 where z3:"⦃ x3 : b3  | c3 ⦄ =  ⦃ z3 : b3  | c3[x3::=V_var z3]cv ⦄ ∧  atom z3 ♯ (x3, v,c3,x1,c1)" using obtain_fresh_z3 by metis

  let ?ft = "(AF_fun_typ x3 (b3[bv3::=b']bb) (c3[bv3::=b']cb) (τ3[bv3::=b']τb) (s3[bv3::=b']sb))"

  have *:"check_fundef Θ Φ (AF_fundef f (AF_fun_typ_some bv3 (AF_fun_typ x3 b3 c3 τ3 s3)))" using ** check_letI lookup_fun_member by metis

  hence ftq:"check_funtypq Θ Φ (AF_fun_typ_some bv3 (AF_fun_typ x3 b3 c3 τ3 s3))" using check_fundef_elims by auto

  let ?ft = "AF_fun_typ_some bv3 (AF_fun_typ x3 b3 c3 τ3 s3)"

  have sup: "supp τ3 ⊆ { atom x3, atom bv3} ∧ supp s3 ⊆ { atom x3, atom bv3 }"  
    using  wfPhi_f_poly_supp_t wfPhi_f_poly_supp_s ** by metis

  have "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let2 x2  τ3[bv3::=b']τb[x3::=v]τv (s3[bv3::=b']sb[x3::=v]sv) s2 ⇐ τ" 
  proof
    show ‹atom x2 ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, τ3[bv3::=b']τb[x3::=v]τv, s3[bv3::=b']sb[x3::=v]sv, τ)› 
    proof -

      have "atom x2 ♯ τ3[bv3::=b']τb[x3::=v]τv" 
        using fresh_subst_v_subst_b subst_v_τ_def subst_b_τ_def ‹ atom x2 ♯ v› sup by fastforce      
      moreover have "atom x2 ♯ s3[bv3::=b']sb[x3::=v]sv" 
        using fresh_subst_v_subst_b subst_v_s_def subst_b_s_def ‹ atom x2 ♯ v› sup 
      proof -
        have "∀b. atom x2 = atom x3 ∨ atom x2 ♯ s3[bv3::=b]b"
          by (metis (no_types) check_letI.hyps(1) fresh_subst_sv_if(1) fresh_subst_v_subst_b insert_commute subst_v_s_def sup) (* 140 ms *)
        then show ?thesis
          by (metis check_letI.hyps(1) fresh_subst_sb_if fresh_subst_sv_if(1) has_subst_b_class.subst_b_fresh_x x_fresh_b) (* 78 ms *)
      qed
      ultimately show ?thesis using fresh_prodN check_letI by metis
    qed

    show ‹ Θ; Φ; {||}; GNil; Δ  ⊢ s3[bv3::=b']sb[x3::=v]sv ⇐ τ3[bv3::=b']τb[x3::=v]τv› proof( rule fundef_poly_check)
      show ‹check_fundef Θ Φ (AF_fundef f (AF_fun_typ_some bv3 (AF_fun_typ x3 b3 c3 τ3 s3)))›   
        using **  lookup_fun_member check_letI by metis
      show ‹Θ ; {||} ; GNil  ⊢ v ⇐ ⦃ x3 : b3[bv3::=b']bb  | c3[bv3::=b']cb ⦄› using ** by metis
      show ‹ Θ ; {||} ; GNil ⊢wf Δ › using ** by metis
      show ‹ Θ ;  {||}  ⊢wf b' ›  using ** by metis
    qed
    show ‹ Θ ; Φ ; {||} ; (x2, b_of τ3[bv3::=b']τb[x3::=v]τv, c_of τ3[bv3::=b']τb[x3::=v]τv x2) #Γ GNil ; Δ  ⊢ s2 ⇐ τ› 
      using check_letI ** b_of.simps c_of.simps subst_defs by metis
  qed

  moreover have "AS_let2 x2  τ3[bv3::=b']τb[x3::=v]τv (s3[bv3::=b']sb[x3::=v]sv) s2 = AS_let2 x   (τ1'[bv1::=b']τb[x1::=v]τv) (s1'[bv1::=b']sb[x1::=v]sv) s" proof -
    have *: "[[atom x2]]lst. s2 = [[atom x]]lst. s" using check_letI  s_branch_s_branch_list.eq_iff by auto
    moreover have " τ3[bv3::=b']τb[x3::=v]τv = τ1'[bv1::=b']τb[x1::=v]τv" using fun_poly_ret_unique ** check_letI by metis
    moreover have "s3[bv3::=b']sb[x3::=v]sv = (s1'[bv1::=b']sb[x1::=v]sv)" using subst_v_flip_eq_two subst_v_s_def  fun_poly_body_unique ** check_letI by metis
    ultimately show ?thesis using s_branch_s_branch_list.eq_iff by metis
  qed

  ultimately show ?case using check_letI by auto
qed(auto+)

lemma check_s_plus:
  assumes "Θ; Φ; {||}; GNil; Δ  ⊢ LET x = (AE_op Plus (V_lit (L_num n1)) (V_lit (L_num n2))) IN s'  ⇐ τ" 
  shows   "Θ; Φ; {||}; GNil; Δ  ⊢ LET x = (AE_val (V_lit (L_num (n1+n2)))) IN s' ⇐ τ"   
proof  -
  obtain t1 where 1: "Θ; Φ; {||}; GNil; Δ  ⊢ AE_op Plus (V_lit (L_num n1)) (V_lit (L_num n2)) ⇒ t1"
    using assms check_s_elims by metis
  then obtain z1 where 2: "t1 =  ⦃ z1 : B_int  | CE_val (V_var z1)  ==  CE_op Plus  ([V_lit (L_num n1)]ce) ([V_lit (L_num n2)]ce)  ⦄"
    using infer_e_plus by metis

  obtain z2 where 3: ‹Θ ; Φ ;  {||} ; GNil ; Δ  ⊢ AE_val (V_lit (L_num (n1+n2))) ⇒ ⦃ z2 : B_int  | CE_val (V_var z2)  ==  CE_val (V_lit (L_num (n1+n2))) ⦄› 
    using infer_v_form infer_e_valI infer_v_litI   infer_l.intros infer_e_wf 1 
    by (simp add: fresh_GNil)

  let ?e = " (AE_op Plus (V_lit (L_num n1)) (V_lit (L_num n2)))"

  show ?thesis proof(rule  subtype_let)
    show "Θ ; Φ ; {||} ; GNil ; Δ  ⊢ LET x = ?e IN s' ⇐ τ" using assms by auto
    show "Θ ; Φ ; {||} ; GNil ; Δ  ⊢ ?e ⇒ t1" using 1 by auto
    show "Θ ; Φ ; {||} ; GNil ; Δ  ⊢ [ [ L_num (n1 + n2) ]v ]e ⇒ ⦃ z2 : B_int  | CE_val (V_var z2)  ==  CE_val (V_lit (L_num (n1+n2))) ⦄" using 3 by auto
    show "Θ ; {||} ; GNil  ⊢  ⦃ z2 : B_int  | CE_val (V_var z2)  ==  CE_val (V_lit (L_num (n1+n2))) ⦄  ≲ t1" using subtype_bop_arith 
      by (metis "1" ‹⋀thesis. (⋀z1. t1 = ⦃ z1 : B_int | [ [ z1 ]v ]ce == [ plus [ [ L_num n1 ]v ]ce [ [ L_num n2 ]v ]ce ]ce ⦄ ⟹ thesis) ⟹ thesis› infer_e_wf(2) opp.distinct(1) type_for_lit.simps(3))
  qed

qed

lemma check_s_leq:
  assumes "Θ ; Φ ;  {||} ; GNil ; Δ  ⊢ LET x = (AE_op LEq (V_lit (L_num n1)) (V_lit (L_num n2))) IN s'  ⇐ τ" 
  shows "Θ; Φ; {||}; GNil; Δ  ⊢ LET x = (AE_val (V_lit (if (n1 ≤ n2) then L_true else L_false))) IN s' ⇐ τ"   
proof -
  obtain t1 where 1: "Θ; Φ; {||}; GNil; Δ  ⊢ AE_op LEq (V_lit (L_num n1)) (V_lit (L_num n2)) ⇒ t1"
    using assms check_s_elims by metis
  then obtain z1 where 2: "t1 =  ⦃ z1 : B_bool  | CE_val (V_var z1)  ==  CE_op LEq  ([V_lit (L_num n1)]ce) ([V_lit (L_num n2)]ce)  ⦄"
    using infer_e_leq by auto

  obtain z2 where 3: ‹Θ ; Φ ;  {||} ; GNil ; Δ  ⊢ AE_val (V_lit ((if (n1 ≤ n2) then L_true else L_false))) ⇒ ⦃ z2 : B_bool  | CE_val (V_var z2)  ==  CE_val (V_lit ((if (n1 ≤ n2) then L_true else L_false))) ⦄› 
    using infer_v_form infer_e_valI infer_v_litI   infer_l.intros infer_e_wf 1 
      fresh_GNil 
    by simp

  show ?thesis proof(rule subtype_let)
    show ‹ Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_op LEq [ L_num n1 ]v [ L_num n2 ]v) s' ⇐ τ› using assms by auto
    show ‹Θ; Φ; {||}; GNil; Δ  ⊢ AE_op LEq [ L_num n1 ]v [ L_num n2 ]v ⇒ t1› using 1 by auto
    show ‹Θ; Φ; {||}; GNil; Δ  ⊢ [ [ if n1 ≤ n2 then L_true else L_false ]v ]e ⇒ ⦃ z2 : B_bool  | CE_val (V_var z2)  ==  CE_val (V_lit ((if (n1 ≤ n2) then L_true else L_false))) ⦄› using 3 by auto
    show ‹Θ ; {||} ; GNil  ⊢ ⦃ z2 : B_bool  | CE_val (V_var z2)  ==  CE_val (V_lit ((if (n1 ≤ n2) then L_true else L_false))) ⦄ ≲ t1› 
      using subtype_bop_arith[where opp=LEq] check_s_wf assms 2  
      by (metis opp.distinct(1) subtype_bop_arith type_l_eq)
  qed
qed

lemma check_s_eq:
  assumes "Θ ; Φ ;  {||} ; GNil ; Δ  ⊢ LET x = (AE_op Eq (V_lit (n1)) (V_lit ( n2))) IN s'  ⇐ τ" 
  shows "Θ; Φ; {||}; GNil; Δ  ⊢ LET x = (AE_val (V_lit (if (n1 = n2) then L_true else L_false))) IN s' ⇐ τ"   
proof -
  obtain t1 where 1: "Θ; Φ; {||}; GNil; Δ  ⊢ AE_op Eq (V_lit (n1)) (V_lit (n2)) ⇒ t1"
    using assms check_s_elims by metis
  then obtain z1 where 2: "t1 =  ⦃ z1 : B_bool  | CE_val (V_var z1)  ==  CE_op Eq  ([V_lit (n1)]ce) ([V_lit (n2)]ce)  ⦄"
    using infer_e_leq by auto

  obtain z2 where 3: ‹Θ ; Φ ;  {||} ; GNil ; Δ  ⊢ AE_val (V_lit ((if (n1 = n2) then L_true else L_false))) ⇒ ⦃ z2 : B_bool  | CE_val (V_var z2)  ==  CE_val (V_lit ((if (n1 = n2) then L_true else L_false))) ⦄› 
    using infer_v_form infer_e_valI infer_v_litI   infer_l.intros infer_e_wf 1 
      fresh_GNil 
    by simp

  show ?thesis proof(rule subtype_let)
    show ‹ Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_op Eq [  n1 ]v [  n2 ]v) s' ⇐ τ› using assms by auto
    show ‹Θ; Φ; {||}; GNil; Δ  ⊢ AE_op Eq [  n1 ]v [  n2 ]v ⇒ t1› using 1 by auto
    show ‹Θ; Φ; {||}; GNil; Δ  ⊢ [ [ if n1 = n2 then L_true else L_false ]v ]e ⇒ ⦃ z2 : B_bool  | CE_val (V_var z2)  ==  CE_val (V_lit ((if (n1 = n2) then L_true else L_false))) ⦄› using 3 by auto
    show ‹Θ ; {||} ; GNil  ⊢ ⦃ z2 : B_bool  | CE_val (V_var z2)  ==  CE_val (V_lit ((if (n1 = n2) then L_true else L_false))) ⦄ ≲ t1› 
    proof -
      have " ⦃ z2 : B_bool  | [ [ z2 ]v ]ce  ==  [ eq [ [ n1 ]v ]ce [ [ n2 ]v ]ce ]ce  ⦄ = t1" using 2 
        by (metis τ_fresh_c fresh_opp_all infer_l_form2 infer_l_fresh ms_fresh_all(31) ms_fresh_all(33) obtain_fresh_z type_e_eq type_l_eq)
      moreover have "Θ ; {||}  ⊢wf GNil" using assms wfX_wfY by fastforce
      moreover have "base_for_lit n1 = base_for_lit n2" using 1 infer_e_wf wfE_elims(12) wfV_elims 
        by metis
      ultimately show ?thesis using subtype_bop_eq[OF ‹Θ ; {||}  ⊢wf GNil›, of n1 n2 z2] by auto     
    qed
  qed
qed

subsection ‹Operators›

lemma preservation_plus:
  assumes "Θ; Φ; Δ ⊢ ⟨ δ , LET x = (AE_op Plus (V_lit (L_num n1)) (V_lit (L_num n2))) IN s' ⟩ ⇐ τ"        
  shows "Θ; Φ; Δ  ⊢ ⟨ δ , LET x =  (AE_val (V_lit (L_num (n1+n2)))) IN s' ⟩ ⇐ τ"
proof -

  have tt: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_op Plus (V_lit (L_num n1)) (V_lit (L_num n2))) s' ⇐ τ" and dsim: "Θ ⊢ δ ∼ Δ" and fd:"(∀fd∈set Φ. check_fundef Θ Φ fd)"
    using assms config_type_elims by blast+

  hence "Θ; Φ; {||}; GNil; Δ  ⊢AS_let x (AE_val (V_lit  (L_num (n1+n2)))) s' ⇐ τ" using check_s_plus assms by auto  

  hence "Θ; Φ; Δ ⊢ ⟨ δ , AS_let x (AE_val (V_lit ( (L_num (n1+n2))))) s' ⟩ ⇐ τ" using dsim config_typeI fd by presburger
  then show ?thesis using dsim config_typeI 
    by (meson order_refl)
qed

lemma preservation_leq:
  assumes "Θ; Φ; Δ ⊢ ⟨ δ , AS_let x (AE_op LEq (V_lit (L_num n1)) (V_lit (L_num n2))) s' ⟩ ⇐ τ"        
  shows "Θ; Φ; Δ  ⊢ ⟨ δ , AS_let x (AE_val (V_lit (((if (n1 ≤ n2) then L_true else L_false))))) s' ⟩ ⇐ τ"
proof -

  have tt: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_op LEq (V_lit (L_num n1)) (V_lit (L_num n2))) s' ⇐ τ" and dsim: "Θ ⊢ δ ∼ Δ" and fd:"(∀fd∈set Φ. check_fundef Θ Φ fd)"
    using assms config_type_elims by blast+

  hence "Θ; Φ; {||}; GNil; Δ  ⊢AS_let x (AE_val (V_lit  ( ((if (n1 ≤ n2) then L_true else L_false))))) s' ⇐ τ" using check_s_leq assms by auto  

  hence "Θ; Φ; Δ ⊢ ⟨ δ , AS_let x (AE_val (V_lit ( (((if (n1 ≤ n2) then L_true else L_false)))))) s' ⟩ ⇐ τ" using dsim config_typeI fd by presburger
  then show ?thesis using dsim config_typeI 
    by (meson order_refl)
qed

lemma preservation_eq:
  assumes "Θ; Φ; Δ ⊢ ⟨ δ , AS_let x (AE_op Eq (V_lit (n1)) (V_lit (n2))) s' ⟩ ⇐ τ"        
  shows "Θ; Φ; Δ  ⊢ ⟨ δ , AS_let x (AE_val (V_lit (((if (n1 = n2) then L_true else L_false))))) s' ⟩ ⇐ τ"
proof -

  have tt: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_op Eq (V_lit (n1)) (V_lit (n2))) s' ⇐ τ" and dsim: "Θ ⊢ δ ∼ Δ" and fd:"(∀fd∈set Φ. check_fundef Θ Φ fd)"
    using assms config_type_elims by blast+

  hence "Θ; Φ; {||}; GNil; Δ  ⊢AS_let x (AE_val (V_lit  ( ((if (n1 = n2) then L_true else L_false))))) s' ⇐ τ" using check_s_eq assms by auto  

  hence "Θ; Φ; Δ ⊢ ⟨ δ , AS_let x (AE_val (V_lit ( (((if (n1 = n2) then L_true else L_false)))))) s' ⟩ ⇐ τ" using dsim config_typeI fd by presburger
  then show ?thesis using dsim config_typeI 
    by (meson order_refl)
qed

subsection ‹Let Statements›

lemma subst_s_abs_lst:
  fixes s::s and sa::s and v'::v
  assumes "[[atom x]]lst. s = [[atom xa]]lst. sa" and "atom xa ♯ v ∧ atom x ♯ v"
  shows "s[x::=v]sv = sa[xa::=v]sv"
proof -
  obtain c'::x where cdash: "atom c' ♯ (v, x, xa, s, sa)" using obtain_fresh by blast    
  moreover have " (x ↔ c') ∙ s = (xa ↔ c') ∙ sa" proof -
    have "atom c' ♯ (s, sa) ∧ atom c' ♯ (x, xa, s, sa)" using cdash by auto
    thus ?thesis using assms by auto
  qed
  ultimately show ?thesis using assms 
    using subst_sv_flip by auto 
qed

lemma check_let_val: 
  fixes v::v and s::s
  shows "Θ ; Φ ; B ; G ; Δ  ⊢ ss ⇐ τ ⟹  B = {||} ⟹ G = GNil ⟹ 
        ss = AS_let x (AE_val v) s ∨  ss = AS_let2 x t (AS_val v) s ⟹  Θ; Φ; {||}; GNil; Δ  ⊢ (s[x::=v]sv) ⇐ τ" and
    "check_branch_s Θ Φ ℬ GNil Δ tid dc const v cs τ ⟹ True" and 
    "check_branch_list Θ Φ ℬ Γ Δ tid dclist v css τ ⟹ True"
proof(nominal_induct τ and τ and τ  avoiding: v rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_letI x1 Θ Φ ℬ Γ Δ e τ z s1 b c)
  hence *:"e = AE_val v" by auto
  let ?G = "(x1, b, c[z::=V_var x1]cv) #Γ Γ"
  have "Θ ; Φ ; ℬ ;  ?G[x1::=v]Γv ; Δ[x1::=v]Δv  ⊢ s1[x1::=v]sv ⇐ τ[x1::=v]τv" 
  proof(rule subst_infer_check_s(1))
    show **:‹ Θ ; ℬ ; Γ ⊢ v ⇒  ⦃ z : b  | c ⦄› using infer_e_elims check_letI * by fast
    thus ‹Θ ; ℬ ; Γ  ⊢  ⦃ z : b  | c ⦄ ≲ ⦃ z : b  | c ⦄› using subtype_reflI  infer_v_wf by metis
    show ‹atom z ♯ (x1, v)› using check_letI fresh_Pair by auto
    show ‹Θ ; Φ ; ℬ ; (x1, b, c[z::=V_var x1]cv) #Γ Γ ; Δ  ⊢ s1 ⇐ τ› using check_letI subst_defs by auto
    show "(x1, b, c[z::=V_var x1]cv) #Γ Γ = GNil @ (x1, b, c[z::=V_var x1]cv) #Γ Γ" by auto
  qed

  hence "Θ ; Φ ; ℬ ;  Γ ; Δ  ⊢ s1[x1::=v]sv ⇐ τ"  using check_letI by auto
  moreover have " s1[x1::=v]sv =  s[x::=v]sv" 
    by (metis (full_types) check_letI fresh_GNil infer_e_elims(7) s_branch_s_branch_list.distinct s_branch_s_branch_list.eq_iff(2) 
        subst_s_abs_lst wfG_x_fresh_in_v_simple)

  ultimately show ?case using check_letI by simp
next
  case (check_let2I x1 Θ Φ ℬ Γ Δ t s1 τ s2 )

  hence s1eq:"s1 = AS_val v" by auto
  let ?G = "(x1, b_of t, c_of t x1) #Γ Γ"
  obtain z::x where *:"atom z ♯ (x1 , v,t)"  using obtain_fresh_z by metis
  hence teq:"t =  ⦃ z : b_of t | c_of t z ⦄" using b_of_c_of_eq by auto
  have "Θ ; Φ ; ℬ ;  ?G[x1::=v]Γv ; Δ[x1::=v]Δv  ⊢ s2[x1::=v]sv ⇐ τ[x1::=v]τv" 
  proof(rule subst_check_check_s(1))
    obtain t' where "Θ ; ℬ ; Γ ⊢ v ⇒ t' ∧  Θ ; ℬ ; Γ ⊢ t' ≲ t" using  check_s_elims(1) check_let2I(10) s1eq by auto
    thus  **:‹ Θ ; ℬ ; Γ ⊢ v ⇐ ⦃ z : b_of t | c_of t z ⦄› using  check_v.intros teq by auto
    show "atom z ♯ (x1, v)" using * by auto
    show ‹  Θ ; Φ ; ℬ ; (x1, b_of t, c_of t x1) #Γ Γ ; Δ  ⊢ s2 ⇐ τ› using check_let2I by auto
    show "(x1, b_of t , c_of t x1) #Γ Γ = GNil @ (x1, b_of t, (c_of t z)[z::=V_var x1]cv) #Γ Γ" using append_g.simps c_of_switch * fresh_prodN by metis
  qed

  hence "Θ ; Φ ; ℬ ;  Γ ; Δ  ⊢ s2[x1::=v]sv ⇐ τ"  using check_let2I by auto
  moreover have " s2[x1::=v]sv =  s[x::=v]sv" using
      check_let2I fresh_GNil check_s_elims s_branch_s_branch_list.distinct s_branch_s_branch_list.eq_iff
      subst_s_abs_lst wfG_x_fresh_in_v_simple
  proof -
    have "AS_let2 x t (AS_val v) s = AS_let2 x1 t s1 s2"
      by (metis check_let2I.prems(3) s_branch_s_branch_list.distinct s_branch_s_branch_list.eq_iff(3)) (* 62 ms *)
    then show ?thesis
      by (metis (no_types) check_let2I check_let2I.prems(2) check_s_elims(1) fresh_GNil s_branch_s_branch_list.eq_iff(3) subst_s_abs_lst wfG_x_fresh_in_v_simple) (* 375 ms *)
  qed

  ultimately show ?case using check_let2I by simp
qed(auto+)

lemma preservation_let_val:
  assumes "Θ; Φ; Δ ⊢ ⟨ δ , AS_let x (AE_val v) s ⟩ ⇐ τ ∨ Θ; Φ; Δ ⊢ ⟨ δ , AS_let2 x t (AS_val v) s ⟩ ⇐ τ" (is "?A ∨ ?B")
  shows " ∃Δ'. Θ; Φ; Δ'  ⊢ ⟨ δ , s[x::=v]sv ⟩ ⇐ τ  ∧ Δ ⊑ Δ'"
proof -
  have tt:  "Θ ⊢ δ ∼ Δ" and fd: "(∀fd∈set Φ. check_fundef Θ Φ fd)"
    using assms by blast+

  have  "?A ∨ ?B" using assms by auto
  then have "Θ; Φ; {||}; GNil; Δ   ⊢  s[x::=v]sv   ⇐ τ"
  proof
    assume "Θ; Φ; Δ ⊢ ⟨ δ , AS_let x (AE_val v) s ⟩ ⇐ τ"
    hence * : " Θ; Φ; {||}; GNil; Δ   ⊢  AS_let x (AE_val v) s  ⇐ τ" by blast
    thus ?thesis using check_let_val by simp
  next
    assume "Θ; Φ; Δ  ⊢ ⟨ δ , AS_let2 x t (AS_val v) s ⟩ ⇐ τ"
    hence * : "Θ; Φ; {||}; GNil; Δ   ⊢  AS_let2 x t (AS_val v) s  ⇐ τ" by blast
    thus ?thesis using check_let_val by simp
  qed

  thus  ?thesis using tt config_typeI fd
      order_refl by metis
qed

lemma check_s_fst_snd:
  assumes "fst_snd = AE_fst ∧ v=v1 ∨ fst_snd = AE_snd ∧ v=v2" 
    and   "Θ; Φ; {||}; GNil; Δ ⊢ AS_let x (fst_snd (V_pair v1 v2)) s' ⇐ τ"
  shows "Θ; Φ; {||}; GNil; Δ ⊢ AS_let x ( AE_val v) s' ⇐ τ"
proof -
  have  1: ‹ Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (fst_snd (V_pair v1 v2)) s' ⇐ τ› using assms by auto

  then obtain t1 where 2:"Θ; Φ; {||}; GNil; Δ  ⊢  (fst_snd (V_pair v1 v2)) ⇒ t1" using check_s_elims by auto

  show ?thesis using subtype_let 1 2 assms 
    by (meson infer_e_fst_pair infer_e_snd_pair)
qed

lemma preservation_fst_snd:
  assumes "Θ; Φ; Δ ⊢ ⟨ δ , LET x = (fst_snd (V_pair v1 v2)) IN s' ⟩ ⇐ τ" and 
    "fst_snd = AE_fst ∧ v=v1 ∨ fst_snd = AE_snd ∧ v=v2"
  shows "∃Δ'. Θ; Φ; Δ ⊢ ⟨ δ , LET x = (AE_val v) IN s' ⟩ ⇐ τ  ∧ Δ ⊑ Δ'"
proof - 
  have  tt: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (fst_snd (V_pair v1 v2)) s' ⇐ τ ∧ Θ ⊢ δ ∼ Δ" using assms by blast
  hence t2: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (fst_snd (V_pair v1 v2)) s' ⇐ τ" by auto

  moreover have "∀fd∈set Φ. check_fundef Θ Φ fd" using assms config_type_elims by auto
  ultimately show ?thesis using config_typeI order_refl tt assms check_s_fst_snd by metis
qed

inductive_cases check_branch_s_elims2[elim!]:
  "Θ ; Φ ;  ℬ ; Γ ; Δ; tid ; cons ; const ; v ⊢ cs ⇐ τ"

lemmas freshers = freshers atom_dom.simps toSet.simps fresh_def x_not_in_b_set
declare freshers [simp]

lemma subtype_eq_if:
  fixes t::τ and va::v
  assumes "Θ ; ℬ ; Γ ⊢wf  ⦃ z : b_of t  | c_of t z ⦄" and "Θ ; ℬ ; Γ ⊢wf ⦃ z : b_of t  | c  IMP c_of t z ⦄ "
  shows   "Θ ; ℬ ; Γ ⊢ ⦃ z : b_of t  | c_of t z ⦄  ≲ ⦃ z : b_of t  | c  IMP c_of t z ⦄ "
proof -
  obtain x::x where xf:"atom x ♯ ((Θ, ℬ, Γ, z, c_of t z, z, c  IMP  c_of t z ),c)" using obtain_fresh by metis

  moreover have "Θ ; ℬ ; (x, b_of t, (c_of t z)[z::=[ x ]v]cv) #Γ Γ  ⊨ (c  IMP  c_of t z )[z::=[ x ]v]cv " 
    unfolding subst_cv.simps 
  proof(rule valid_eq_imp)

    have "Θ ; ℬ ; (x, b_of t, (c_of t z)[z::=[ x ]v]v) #Γ Γ   ⊢wf (c  IMP  (c_of t z))[z::=[ x ]v]v    " 
      apply(rule  wfT_wfC_cons)
      apply(simp add: assms, simp add: assms, unfold fresh_prodN )
      using  xf fresh_prodN by metis+     
    thus "Θ ; ℬ ; (x, b_of t, (c_of t z)[z::=[ x ]v]cv) #Γ Γ   ⊢wf c[z::=[ x ]v]cv  IMP  (c_of t z)[z::=[ x ]v]cv " 
      using subst_cv.simps subst_defs by auto
  qed

  ultimately show ?thesis using subtype_baseI assms fresh_Pair subst_defs by metis
qed

lemma subtype_eq_if_τ:
  fixes t::τ and va::v
  assumes "Θ ; ℬ ; Γ ⊢wf  t" and "Θ ; ℬ ; Γ ⊢wf ⦃ z : b_of t  | c  IMP c_of t z ⦄ " and "atom z ♯ t"
  shows   "Θ ; ℬ ; Γ ⊢ t  ≲ ⦃ z : b_of t  | c  IMP c_of t z ⦄ "
proof -
  have "t = ⦃ z : b_of t | c_of t z ⦄" using b_of_c_of_eq assms by auto
  thus ?thesis  using subtype_eq_if assms  c_of.simps b_of.simps by metis
qed

lemma valid_conj:
  assumes  "Θ ; ℬ ; Γ ⊨ c1" and "Θ ; ℬ ; Γ ⊨ c2" 
  shows "Θ ; ℬ ; Γ ⊨ c1 AND c2" 
proof
  show ‹ Θ ; ℬ ; Γ   ⊢wf c1  AND  c2  › using valid.simps wfC_conjI assms by auto
  show ‹∀i.  Θ ; Γ ⊢ i ∧  i ⊨ Γ  ⟶  i ⊨ c1  AND  c2  › 
  proof(rule+)
    fix i
    assume *:"Θ ; Γ ⊢ i ∧ i ⊨ Γ " 
    thus "i ⟦ c1 ⟧ ~ True" using assms valid.simps 
      using is_satis.cases by blast
    show "i ⟦ c2 ⟧ ~ True" using assms valid.simps 
      using is_satis.cases * by blast  
  qed
qed

subsection ‹Other Statements›

lemma check_if:
  fixes s'::s and cs::branch_s and css::branch_list and v::v
  shows    "Θ; Φ; B; G; Δ ⊢  s' ⇐ τ ⟹ s' =  IF (V_lit ll) THEN s1 ELSE s2 ⟹  
        Θ ; {||} ; GNil  ⊢wf τ ⟹ G = GNil ⟹ B = {||} ⟹ ll = L_true ∧ s = s1 ∨ ll = L_false ∧ s = s2 ⟹ 
        Θ; Φ; {||}; GNil; Δ  ⊢  s ⇐ τ" and
    "check_branch_s Θ Φ  {||} GNil Δ tid dc const v cs τ ⟹ True" and 
    "check_branch_list Θ Φ  {||} Γ Δ tid dclist v css τ ⟹ True"
proof(nominal_induct τ and τ and τ  rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_ifI z Θ Φ ℬ Γ Δ v s1 s2 τ)
  obtain z' where teq: "τ = ⦃ z' : b_of τ | c_of τ z' ⦄ ∧ atom z' ♯ (z,τ)" using obtain_fresh_z_c_of by metis
  hence ceq: "(c_of τ z')[z'::=[ z ]v]cv = (c_of τ z)" using c_of_switch fresh_Pair by metis
  have zf: " atom z ♯ c_of τ z'"
    using c_of_fresh check_ifI teq fresh_Pair fresh_at_base by metis
  hence 1:"Θ; Φ; {||}; GNil; Δ  ⊢ s ⇐  ⦃ z : b_of τ  | CE_val (V_lit ll)  ==  CE_val (V_lit ll)  IMP  c_of τ z  ⦄" using check_ifI by auto
  moreover have 2:"Θ ; {||} ; GNil ⊢ (⦃ z : b_of τ  | CE_val (V_lit ll)  ==  CE_val (V_lit ll)  IMP  c_of τ z  ⦄) ≲  τ" 
  proof - 
    have "Θ ; {||} ; GNil ⊢wf (⦃ z : b_of τ  | CE_val (V_lit ll )  ==  CE_val (V_lit ll)   IMP c_of τ z  ⦄)" using check_ifI check_s_wf by auto
    moreover have "Θ ; {||} ; GNil  ⊢wf τ" using  check_s_wf check_ifI by auto
    ultimately show ?thesis using subtype_if_simp[of Θ " {||}" z "b_of τ" ll "c_of τ z'" z'] using teq ceq zf subst_defs by metis
  qed
  ultimately show ?case  using check_s_supertype(1) check_ifI by metis
qed(auto+)

lemma preservation_if: 
  assumes  "Θ; Φ; Δ ⊢ ⟨ δ , IF (V_lit ll) THEN s1 ELSE s2 ⟩ ⇐ τ" and 
    "ll = L_true ∧ s = s1 ∨ ll = L_false ∧ s = s2"
  shows "Θ; Φ; Δ  ⊢ ⟨δ, s⟩ ⇐ τ  ∧ setD Δ ⊆ setD Δ"
proof -
  have *: "Θ; Φ; {||}; GNil; Δ  ⊢  AS_if (V_lit ll) s1 s2 ⇐ τ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using assms config_type_elims by metis
  hence "Θ; Φ; {||}; GNil; Δ  ⊢  s ⇐ τ" using check_s_wf check_if assms by metis
  hence "Θ; Φ; Δ ⊢ ⟨δ, s⟩ ⇐ τ  ∧ setD Δ ⊆ setD Δ" using config_typeI * 
    using assms(1) by blast
  thus ?thesis by blast
qed

lemma wfT_conj:
  assumes "Θ ; ℬ ; GNil ⊢wf ⦃ z : b | c1 ⦄" and  "Θ ; ℬ ; GNil ⊢wf ⦃ z : b | c2 ⦄"
  shows  "Θ ; ℬ ; GNil ⊢wf ⦃ z : b | c1 AND c2⦄"
proof
  show ‹atom z ♯ (Θ, ℬ, GNil)›
    apply(unfold fresh_prodN, intro conjI) 
    using wfTh_fresh wfT_wf assms apply metis
    using fresh_GNil x_not_in_b_set fresh_def by metis+   
  show ‹ Θ ; ℬ  ⊢wf b › using wfT_elims assms by metis
  have "Θ ; ℬ ; (z, b, TRUE) #Γ GNil   ⊢wf c1" using wfT_wfC fresh_GNil assms by auto
  moreover have "Θ ; ℬ ; (z, b, TRUE) #Γ GNil   ⊢wf c2" using wfT_wfC fresh_GNil assms by auto
  ultimately show ‹ Θ ; ℬ ; (z, b, TRUE) #Γ GNil   ⊢wf c1  AND  c2  › using wfC_conjI by auto
qed

lemma subtype_conj:
  assumes    "Θ ; ℬ ; GNil  ⊢ t ≲ ⦃ z : b | c1 ⦄" and   "Θ ; ℬ ; GNil  ⊢ t ≲ ⦃ z : b | c2 ⦄" 
  shows   "Θ ; ℬ ; GNil  ⊢ ⦃ z : b | c_of t z ⦄  ≲ ⦃ z : b | c1 AND c2 ⦄" 
proof -
  have beq: "b_of t = b" using subtype_eq_base2 b_of.simps assms by metis
  obtain x::x where x:‹atom x ♯ (Θ, ℬ, GNil, z, c_of t z, z, c1  AND  c2 )› using obtain_fresh by metis
  thus ?thesis proof
    have "atom z ♯ t" using subtype_wf wfT_supp fresh_def x_not_in_b_set atom_dom.simps toSet.simps assms dom.simps by fastforce
    hence t:"t = ⦃ z : b_of t  | c_of t z ⦄" using b_of_c_of_eq by auto
    thus  ‹ Θ ; ℬ ; GNil   ⊢wf ⦃ z : b  | c_of t z ⦄ › using subtype_wf beq assms by auto

    show ‹Θ ; ℬ ; (x, b, (c_of t z)[z::=[ x ]v]v) #Γ GNil  ⊨ (c1  AND  c2 )[z::=[ x ]v]v ›      
    proof -
      have ‹Θ ; ℬ ; (x, b, (c_of t z)[z::=[ x ]v]v) #Γ GNil  ⊨ c1[z::=[ x ]v]v ›
      proof(rule subtype_valid)
        show ‹Θ ; ℬ ; GNil  ⊢ t ≲ ⦃ z : b | c1 ⦄› using assms by auto
        show ‹atom x ♯ GNil› using fresh_GNil by auto
        show ‹t = ⦃ z : b  | c_of t z ⦄› using t beq by auto
        show ‹⦃ z : b  | c1 ⦄ = ⦃ z : b  | c1 ⦄› by auto
      qed
      moreover have ‹Θ ; ℬ ; (x, b, (c_of t z)[z::=[ x ]v]v) #Γ GNil  ⊨ c2[z::=[ x ]v]v ›
      proof(rule subtype_valid)
        show ‹Θ ; ℬ ; GNil  ⊢ t ≲ ⦃ z : b | c2 ⦄› using assms by auto
        show ‹atom x ♯ GNil› using fresh_GNil by auto
        show ‹t = ⦃ z : b  | c_of t z ⦄› using t beq by auto
        show ‹⦃ z : b  | c2 ⦄ = ⦃ z : b  | c2 ⦄› by auto
      qed
      ultimately show ?thesis unfolding subst_cv.simps subst_v_c_def  using valid_conj by metis
    qed
    thus ‹ Θ ; ℬ ; GNil   ⊢wf ⦃ z : b  | c1  AND  c2  ⦄ › using subtype_wf wfT_conj assms by auto
  qed
qed

lemma infer_v_conj:
  assumes "Θ ; ℬ ; GNil  ⊢ v ⇐ ⦃ z : b | c1 ⦄" and "Θ ; ℬ ; GNil  ⊢ v ⇐ ⦃ z : b | c2 ⦄"
  shows "Θ ; ℬ ; GNil  ⊢ v ⇐ ⦃ z : b | c1 AND c2 ⦄" 
proof -
  obtain t1 where t1: "Θ ; ℬ ; GNil  ⊢ v ⇒ t1 ∧ Θ ; ℬ ; GNil ⊢ t1 ≲ ⦃ z : b | c1 ⦄" 
    using assms check_v_elims by metis
  obtain t2 where t2: "Θ ; ℬ ; GNil  ⊢ v ⇒ t2 ∧ Θ ; ℬ ; GNil ⊢ t2 ≲ ⦃ z : b | c2 ⦄" 
    using assms check_v_elims by metis
  have teq: "t1 = ⦃ z : b | c_of t1 z ⦄" using subtype_eq_base2 b_of.simps 
    by (metis (full_types) b_of_c_of_eq fresh_GNil infer_v_t_wf t1 wfT_x_fresh)
  have "t1 = t2" using infer_v_uniqueness t1 t2 by auto
  hence " Θ ; ℬ ; GNil ⊢ ⦃ z : b | c_of t1 z ⦄ ≲ ⦃ z : b | c1 AND c2 ⦄" using subtype_conj t1 t2 by simp
  hence " Θ ; ℬ ; GNil ⊢ t1 ≲ ⦃ z : b | c1 AND c2 ⦄" using teq by auto
  thus ?thesis using t1 using check_v.intros by auto
qed

lemma wfG_conj:
  fixes c1::c
  assumes  "Θ ; ℬ  ⊢wf (x, b, c1 AND c2) #Γ Γ"
  shows "Θ ; ℬ  ⊢wf (x, b, c1) #Γ Γ"
proof(cases "c1 ∈ {TRUE, FALSE}")
  case True
  then show ?thesis using assms wfG_cons2I  wfG_elims wfX_wfY by metis
next
  case False
  then show ?thesis using assms wfG_cons1I  wfG_elims wfX_wfY wfC_elims 
    by (metis wfG_elim2)
qed

lemma check_match:
  fixes s'::s and s::s and css::branch_list and cs::branch_s
  shows "Θ ; Φ ; ℬ ; Γ ; Δ ⊢  s ⇐ τ ⟹ True" and
    "Θ ; Φ ; B ; G ; Δ ; tid ; dc ; const  ;  vcons ⊢  cs ⇐  τ ⟹ 
             vcons = V_cons tid dc v ⟹ B =  {||} ⟹ G = GNil ⟹ cs =  (dc x' ⇒ s') ⟹  
             Θ ; {||} ; GNil ⊢ v ⇐ const ⟹ 
             Θ; Φ; {||}; GNil; Δ  ⊢ s'[x'::=v]sv ⇐ τ" and
    "Θ ; Φ ; B ; G ; Δ ; tid ; dclist ; vcons  ⊢ css ⇐ τ ⟹ distinct (map fst dclist) ⟹
             vcons = V_cons tid dc v ⟹ B =  {||} ⟹ (dc, const) ∈ set dclist ⟹ G = GNil ⟹ 
             Some (AS_branch dc x' s') = lookup_branch dc css ⟹ Θ ; {||} ; GNil ⊢ v ⇐ const ⟹ 
             Θ; Φ; {||}; GNil; Δ  ⊢ s'[x'::=v]sv ⇐ τ"
proof(nominal_induct τ and τ and τ avoiding: x' v  rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_branch_list_consI Θ Φ ℬ Γ Δ tid consa consta va cs τ dclist cssa)

  then obtain xa and sa where cseq:"cs = AS_branch consa xa sa" using check_branch_s_elims2[OF check_branch_list_consI(1)] by metis

  show ?case proof(cases "dc = consa")
    case True
    hence "cs = AS_branch consa x' s'" using check_branch_list_consI cseq 
      by (metis lookup_branch.simps(2) option.inject)
    moreover have "const = consta" using check_branch_list_consI distinct.simps 
      by (metis True dclist_distinct_unique list.set_intros(1))
    moreover have "va = V_cons tid consa v" using check_branch_list_consI True by auto
    ultimately  show ?thesis using check_branch_list_consI  by auto
  next
    case False
    hence "Some (AS_branch dc x' s') = lookup_branch dc cssa" using lookup_branch.simps(2) check_branch_list_consI(10) cseq by auto
    moreover have "(dc, const) ∈ set dclist" using check_branch_list_consI False by simp
    ultimately show ?thesis using check_branch_list_consI by auto
  qed

next
  case (check_branch_list_finalI Θ Φ ℬ Γ Δ tid cons const va cs τ)
  hence " cs = AS_branch cons x' s'" using lookup.simps check_branch_list_finalI lookup_branch.simps option.inject 
    by (metis map_of.simps(1) map_of_Cons_code(2) option.distinct(1) s_branch_s_branch_list.exhaust(2) weak_map_of_SomeI)
  then show ?case using check_branch_list_finalI by auto
next
  case (check_branch_s_branchI Θ ℬ Γ Δ τ const x Φ tid cons va s)

  text ‹Supporting facts here to make the main body of the proof concise›
  have xf:"atom x ♯ τ" proof -
    have "supp τ ⊆ supp  ℬ" using wf_supp(4) check_branch_s_branchI  atom_dom.simps toSet.simps dom.simps by fastforce
    thus ?thesis using fresh_def x_not_in_b_set by blast
  qed

  hence "τ[x::=v]τv = τ" using forget_subst_v subst_v_τ_def by auto
  have "Δ[x::=v]Δv = Δ" using forget_subst_dv  wfD_x_fresh fresh_GNil check_branch_s_branchI by metis

  have "supp v = {}" using check_branch_s_branchI check_v_wf wfV_supp_nil by metis
  hence "supp va = {}" using ‹ va = V_cons tid cons v› v.supp pure_supp by auto

  let ?G = "(x, b_of const, [ va ]ce  ==  [ V_cons tid cons [ x ]v ]ce   AND c_of const x ) #Γ Γ"
  obtain z::x where z: "const = ⦃ z : b_of const | c_of const z ⦄ ∧ atom z ♯ (x', v,x,const,va)" 
    using obtain_fresh_z_c_of by metis

  have  vt: ‹Θ ; ℬ ; GNil  ⊢ v ⇐ ⦃ z : b_of const  | [ va ]ce  ==  [ V_cons tid cons [ z ]v ]ce  AND c_of const z ⦄›
  proof(rule infer_v_conj)
    obtain t' where t: "Θ ; ℬ ; GNil  ⊢ v ⇒ t' ∧ Θ ; ℬ ; GNil ⊢ t' ≲ const" 
      using check_v_elims check_branch_s_branchI by metis
    show "Θ ; ℬ ; GNil  ⊢ v ⇐ ⦃ z : b_of const  | [ va ]ce  ==  [ V_cons tid cons [ z ]v ]ce  ⦄"        
    proof(rule check_v_top)

      show "Θ ; ℬ ; GNil   ⊢wf ⦃ z : b_of const  | [ va ]ce  ==  [ V_cons tid cons [ z ]v ]ce  ⦄ "     

      proof(rule wfG_wfT)
        show ‹ Θ ; ℬ  ⊢wf (x, b_of const, ([ va ]ce  ==  [ V_cons tid cons [ z ]v ]ce    )[z::=[ x ]v]cv) #Γ GNil ›
        proof -
          have 1: "va[z::=[ x ]v]vv  = va" using  forget_subst_v subst_v_v_def  z fresh_prodN by metis
          moreover have 2: "Θ ; ℬ  ⊢wf (x, b_of const, [ va ]ce  ==  [ V_cons tid cons [ x ]v ]ce   AND  c_of const x ) #Γ GNil  "
            using    check_branch_s_branchI(17)[THEN check_s_wf] ‹Γ = GNil› by auto      
          moreover hence "Θ ; ℬ  ⊢wf (x, b_of const, [ va ]ce  ==  [ V_cons tid cons [ x ]v ]ce ) #Γ GNil" 
            using wfG_conj by metis
          ultimately show ?thesis
            unfolding subst_cv.simps subst_cev.simps subst_vv.simps by auto
        qed      
        show ‹atom x ♯ ([ va ]ce  ==  [ V_cons tid cons [ z ]v ]ce   )› unfolding c.fresh ce.fresh v.fresh
          apply(intro conjI )        
          using  check_branch_s_branchI fresh_at_base z freshers apply simp
          using  check_branch_s_branchI fresh_at_base z freshers apply simp
          using pure_supp apply force
          using z fresh_x_neq fresh_prod5 by metis        
      qed
      show ‹[ va ]ce = [ V_cons tid cons [ z ]v ]ce[z::=v]cev› 
        using ‹ va = V_cons tid cons v› subst_cev.simps subst_vv.simps by auto
      show ‹ Θ ; ℬ ; GNil ⊢ v ⇐ const › using check_branch_s_branchI by auto
      show "supp [ va ]ce ⊆ supp ℬ" using ‹supp va = {}› ce.supp by simp
    qed
    show "Θ ; ℬ ; GNil  ⊢ v ⇐ ⦃ z : b_of const  | c_of const z ⦄" 
      using check_branch_s_branchI z by auto
  qed

  text ‹Main body of proof for this case›
  have "Θ ; Φ ; ℬ ; (?G)[x::=v]Γv ; Δ[x::=v]Δv  ⊢ s[x::=v]sv ⇐ τ[x::=v]τv"
  proof(rule subst_check_check_s)
    show ‹Θ ; ℬ ; GNil  ⊢ v ⇐ ⦃ z : b_of const  | [ va ]ce  ==  [ V_cons tid cons [ z ]v ]ce   AND c_of const z ⦄› using vt by auto
    show ‹atom z ♯ (x, v)› using z fresh_prodN by auto
    show ‹ Θ ; Φ ; ℬ ; ?G ; Δ  ⊢ s ⇐ τ› 
      using check_branch_s_branchI by auto

    show ‹ ?G = GNil @ (x, b_of const, ([ va ]ce  ==  [ V_cons tid cons [ z ]v ]ce   AND c_of const z)[z::=[ x ]v]cv) #Γ GNil›      
    proof -
      have "va[z::=[ x ]v]vv  = va" using  forget_subst_v subst_v_v_def  z fresh_prodN by metis
      moreover have  "(c_of const z)[z::=[ x ]v]cv = c_of const x" 
        using  c_of_switch[of z const x]  z fresh_prodN by metis
      ultimately show ?thesis
        unfolding subst_cv.simps subst_cev.simps subst_vv.simps append_g.simps         
        using c_of_switch[of z const x]  z fresh_prodN z fresh_prodN  check_branch_s_branchI by argo
    qed
  qed
  moreover have "s[x::=v]sv = s'[x'::=v]sv" 
    using check_branch_s_branchI subst_v_flip_eq_two subst_v_s_def s_branch_s_branch_list.eq_iff by metis
  ultimately show  ?case using  check_branch_s_branchI ‹τ[x::=v]τv = τ› ‹Δ[x::=v]Δv = Δ› by auto
qed(auto+)

text ‹Lemmas for while reduction. Making these separate lemmas allows flexibility in wiring them into the main proof and robustness
if we change it›

lemma check_unit:
  fixes τ::τ and Φ::Φ and Δ::Δ and G::Γ
  assumes "Θ ; {||} ; GNil  ⊢ ⦃ z : B_unit  | TRUE ⦄ ≲ τ'" and "Θ ; {||} ; GNil ⊢wf Δ"  and "Θ  ⊢wf Φ"  and "Θ ; {||} ⊢wf G"
  shows ‹ Θ ; Φ ; {||} ; G ; Δ  ⊢ [[ L_unit ]v]s ⇐ τ'›
proof - 
  have *:"Θ ; {||} ; GNil  ⊢ [L_unit]v ⇒ ⦃ z : B_unit  | [ [ z ]v ]ce  ==  [ [ L_unit ]v ]ce  ⦄" 
    using infer_l.intros(4) infer_v_litI fresh_GNil assms  wfX_wfY   by (meson subtype_g_wf)
  moreover have "Θ ; {||} ; GNil  ⊢ ⦃ z : B_unit  | [ [ z ]v ]ce  ==  [ [ L_unit ]v ]ce  ⦄ ≲ τ'" 
    using subtype_top subtype_trans * infer_v_wf 
    by (meson assms(1))
  ultimately show ?thesis (*apply(rule check_valI, auto simp add: assms,rule * )*)
    using subtype_top subtype_trans fresh_GNil assms check_valI assms check_s_g_weakening assms toSet.simps 
    by (metis bot.extremum infer_v_g_weakening subtype_weakening wfD_wf)
qed

lemma preservation_var:
  shows "Θ; Φ; {||}; GNil; Δ  ⊢ VAR u : τ' = v IN s ⇐ τ ⟹ Θ ⊢ δ ∼ Δ ⟹ atom u ♯ δ ⟹ atom u ♯ Δ ⟹
         Θ; Φ; {||}; GNil; (u,τ')#ΔΔ  ⊢ s ⇐ τ ∧ Θ ⊢ (u,v)#δ ∼ (u,τ')#ΔΔ"
    and
    "check_branch_s Θ Φ  {||} GNil Δ tid dc const v cs τ ⟹ True" and 
    "check_branch_list Θ Φ  {||} Γ Δ tid dclist v css τ ⟹ True"
proof(nominal_induct  "{||}::bv fset" GNil Δ "VAR u : τ' = v IN s" τ and τ and τ  rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_varI u' Θ Φ Δ τ s')
  hence "Θ; Φ; {||}; GNil; (u, τ') #Δ Δ  ⊢ s ⇐ τ" using check_s_abs_u check_v_wf by metis

  moreover have "Θ ⊢ ((u,v)#δ) ∼ ((u,τ')#ΔΔ)" proof
    show ‹Θ  ⊢ δ ∼ Δ › using check_varI by auto
    show ‹Θ ; {||} ; GNil  ⊢ v ⇐ τ'› using check_varI by auto
    show ‹u ∉ fst ` set δ› using check_varI fresh_d_fst_d by auto
  qed

  ultimately show ?case by simp
qed(auto+)

lemma check_while:
  shows "Θ; Φ; {||}; GNil; Δ  ⊢ WHILE s1 DO { s2 }  ⇐ τ ⟹ atom x ♯ (s1, s2) ⟹  atom z' ♯ x ⟹
       Θ; Φ; {||}; GNil; Δ  ⊢ LET x : (⦃ z' : B_bool  | TRUE ⦄) = s1 IN (IF (V_var x) THEN (s2 ;; (WHILE s1 DO {s2}))  
            ELSE ([ V_lit L_unit]s))  ⇐ τ" and
    "check_branch_s Θ Φ  {||} GNil Δ tid dc const v cs τ ⟹ True" and 
    "check_branch_list Θ Φ  {||} Γ Δ tid dclist v css τ ⟹ True"
proof(nominal_induct  "{||}::bv fset" GNil Δ "AS_while s1 s2" τ and τ and τ  avoiding: s1 s2 x z' rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_whileI Θ Φ Δ s1 z s2 τ')
  have teq:"⦃ z' : B_bool  | TRUE ⦄ = ⦃ z : B_bool  | TRUE ⦄" using τ.eq_iff by auto

  show ?case proof
    have " atom x ♯ τ' " using wfT_nil_supp fresh_def subtype_wfT check_whileI(5) by fast
    moreover have "atom x ♯ ⦃ z' : B_bool  | TRUE ⦄ " using τ.fresh c.fresh b.fresh by metis  
    ultimately show ‹atom x ♯ (Θ, Φ,  {||}, GNil, Δ, ⦃ z' : B_bool  | TRUE ⦄, s1, τ')›
      apply(unfold fresh_prodN)  
      using check_whileI  wb_x_fresh check_s_wf wfD_x_fresh fresh_empty_fset fresh_GNil fresh_Pair ‹atom x ♯ τ'›  by metis

    show ‹ Θ ; Φ ;  {||} ; GNil ; Δ  ⊢ s1 ⇐ ⦃ z' : B_bool  | TRUE ⦄› using check_whileI  teq by metis

    let ?G =  "(x, b_of ⦃ z' : B_bool  | TRUE ⦄, c_of ⦃ z' : B_bool  | TRUE ⦄ x) #Γ GNil"

    have cof:"(c_of ⦃ z' : B_bool  | TRUE ⦄ x) = C_true" using c_of.simps check_whileI subst_cv.simps by metis
    have  wfg: "Θ ;  {||} ⊢wf ?G" proof 
      show "c_of ⦃ z' : B_bool  | TRUE ⦄ x ∈ {TRUE, FALSE}" using subst_cv.simps cof by auto
      show "Θ ;  {||} ⊢wf GNil " using wfG_nilI check_whileI wfX_wfY check_s_wf by metis
      show "atom x ♯ GNil" using fresh_GNil by auto
      show "Θ ;  {||} ⊢wf b_of ⦃ z' : B_bool  | TRUE ⦄  " using wfB_boolI wfX_wfY check_s_wf b_of.simps 
        by (metis ‹Θ ; {||} ⊢wf GNil›)
    qed

    obtain zz::x where zf:‹atom zz ♯ ((Θ, Φ, {||}::bv fset, ?G , Δ, [ x ]v, 
                                  AS_seq s2 (AS_while s1 s2), AS_val [ L_unit ]v, τ'),x,?G)›
      using obtain_fresh by blast
    show ‹ Θ ; Φ ;  {||} ; ?G ; Δ  ⊢ 
                   AS_if [ x ]v (AS_seq s2 (AS_while s1 s2)) (AS_val [ L_unit ]v) ⇐ τ'› 
    proof      
      show "atom zz ♯ (Θ, Φ, {||}::bv fset, ?G , Δ, [ x ]v, AS_seq s2 (AS_while s1 s2), AS_val [ L_unit ]v, τ')" using zf by auto
      show ‹Θ ; {||} ; ?G  ⊢ [ x ]v ⇐ ⦃ zz : B_bool  | TRUE ⦄› proof
        have "atom zz ♯ x ∧ atom zz ♯ (Θ,  {||}::bv fset, ?G)" using zf fresh_prodN by metis
        thus ‹ Θ ; {||} ; ?G  ⊢ [ x ]v ⇒⦃ zz : B_bool |  [[zz]v]ce == [[ x ]v]ce  ⦄› 
          using infer_v_varI lookup.simps wfg b_of.simps by metis
        thus  ‹Θ ; {||} ; ?G  ⊢ ⦃ zz : B_bool |  [[ zz ]v]ce == [[ x ]v]ce ⦄  ≲ ⦃ zz : B_bool  | TRUE ⦄›
          using subtype_top infer_v_wf by metis
      qed 
      show ‹ Θ ; Φ ; {||} ; ?G ; Δ  ⊢ AS_seq s2 (AS_while s1 s2) ⇐ ⦃ zz : b_of τ'  | [ [ x ]v ]ce  ==  [ [ L_true ]v ]ce   IMP  c_of τ' zz  ⦄› 
      proof 
        have "⦃ zz : B_unit  | TRUE ⦄ = ⦃ z : B_unit  | TRUE ⦄" using τ.eq_iff by auto 
        thus ‹ Θ ; Φ ; {||} ; ?G ; Δ  ⊢ s2 ⇐ ⦃ zz : B_unit  | TRUE ⦄› using check_s_g_weakening(1) [OF check_whileI(3) _ wfg] toSet.simps 
          by (simp add: ‹⦃ zz : B_unit | TRUE ⦄ = ⦃ z : B_unit | TRUE ⦄›)

        show ‹ Θ ; Φ ; {||} ; ?G ; Δ  ⊢ AS_while s1 s2 ⇐ ⦃ zz : b_of τ'  | [ [ x ]v ]ce  ==  [ [ L_true ]v ]ce   IMP  c_of τ' zz  ⦄›
        proof(rule check_s_supertype(1))
          have ‹ Θ; Φ; {||}; GNil; Δ  ⊢ AS_while s1 s2 ⇐ τ'› using  check_whileI by auto
          thus *:‹ Θ ; Φ ; {||} ; ?G ; Δ  ⊢ AS_while s1 s2 ⇐ τ' › using  check_s_g_weakening(1)[OF _ _ wfg] toSet.simps by auto

          show ‹Θ ; {||} ; ?G  ⊢ τ'  ≲ ⦃ zz : b_of τ'  | [ [ x ]v ]ce  ==  [ [ L_true ]v ]ce   IMP  c_of τ' zz  ⦄› 
          proof(rule subtype_eq_if_τ)
            show ‹ Θ ; {||} ; ?G ⊢wf τ' › using * check_s_wf by auto
            show ‹ Θ ; {||} ; ?G  ⊢wf ⦃ zz : b_of τ'  | [ [ x ]v ]ce  ==  [ [ L_true ]v ]ce   IMP  c_of τ' zz  ⦄ ›
              apply(rule wfT_eq_imp, simp add: base_for_lit.simps)
              using subtype_wf check_whileI wfg zf fresh_prodN by metis+
            show ‹atom zz ♯ τ'› using  zf fresh_prodN by metis
          qed
        qed

      qed
      show ‹ Θ ; Φ ; {||} ; ?G ; Δ  ⊢ AS_val [ L_unit ]v ⇐ ⦃ zz : b_of τ'  | [ [ x ]v ]ce  ==  [ [ L_false ]v ]ce   IMP  c_of τ' zz  ⦄›
      proof(rule check_s_supertype(1))

        show *:‹ Θ ; Φ ; {||} ; ?G ; Δ  ⊢ AS_val [ L_unit ]v ⇐ τ'› 
          using check_unit[OF check_whileI(5) _ _ wfg] using check_whileI wfg wfX_wfY check_s_wf by metis
        show ‹Θ ; {||} ; ?G  ⊢ τ' ≲ ⦃ zz : b_of τ'  | [ [ x ]v ]ce  ==  [ [ L_false ]v ]ce   IMP  c_of τ' zz  ⦄› 
        proof(rule subtype_eq_if_τ)
          show ‹ Θ ; {||} ; ?G ⊢wf τ' › using * check_s_wf by metis
          show ‹ Θ ; {||} ; ?G  ⊢wf ⦃ zz : b_of τ'  | [ [ x ]v ]ce  ==  [ [ L_false ]v ]ce   IMP  c_of τ' zz  ⦄ ›                          
            apply(rule wfT_eq_imp, simp add: base_for_lit.simps)
            using subtype_wf check_whileI wfg zf fresh_prodN by metis+
          show ‹atom zz ♯ τ'› using  zf fresh_prodN by metis
        qed
      qed
    qed
  qed
qed(auto+)

lemma check_s_narrow:
  fixes s::s and x::x
  assumes "atom x ♯ (Θ, Φ, ℬ, Γ, Δ, c, τ, s)" and "Θ ; Φ ; ℬ ; (x, B_bool, c) #Γ Γ ; Δ  ⊢ s ⇐ τ" and    
    "Θ ; ℬ ; Γ  ⊨ c "
  shows "Θ ; Φ ; ℬ ;  Γ ; Δ  ⊢ s ⇐ τ"
proof -
  let ?B = "({||}::bv fset)"
  let ?v = "V_lit L_true"

  obtain z::x where z: "atom z ♯ (x, [ L_true ]v,c)" using obtain_fresh by metis

  have "atom z ♯ c" using z fresh_prodN by auto
  hence c:"  c[x::=[ z ]v]v[z::=[ x ]v]cv = c" using  subst_v_c_def by simp

  have "Θ ; Φ ; ℬ ; ((x,B_bool, c) #Γ Γ)[x::=?v]Γv ; Δ[x::=?v]Δv   ⊢  s[x::=?v]sv   ⇐ τ[x::=?v]τv" proof(rule  subst_infer_check_s(1) )
    show vt: ‹ Θ ; ℬ ; Γ  ⊢ [ L_true ]v ⇒ ⦃ z : B_bool | (CE_val (V_var z)) == (CE_val (V_lit  L_true )) ⦄   › 
      using infer_v_litI check_s_wf wfG_elims(2) infer_trueI assms by metis     
    show ‹Θ ; ℬ ; Γ  ⊢ ⦃ z : B_bool | (CE_val (V_var z)) == (CE_val (V_lit  L_true )) ⦄ ≲ ⦃ z : B_bool  | c[x::=[ z ]v]v ⦄› proof
      show ‹atom x ♯ (Θ, ℬ, Γ, z, [ [ z ]v ]ce  ==  [ [ L_true ]v ]ce , z, c[x::=[ z ]v]v)› 
        apply(unfold fresh_prodN, intro conjI) 
        prefer 5
        using c.fresh ce.fresh v.fresh z fresh_prodN apply auto[1]
        prefer 6
        using fresh_subst_v_if[of "atom x" c x] assms fresh_prodN apply simp
        using z assms fresh_prodN apply metis
        using z  assms fresh_prodN apply metis
        using z assms  fresh_prodN apply metis
        using z fresh_prodN assms fresh_at_base by metis+
      show ‹ Θ ; ℬ ; Γ   ⊢wf ⦃ z : B_bool  | [ [ z ]v ]ce  ==  [ [ L_true ]v ]ce  ⦄ › using vt infer_v_wf by simp
      show ‹ Θ ; ℬ ; Γ   ⊢wf ⦃ z : B_bool  | c[x::=[ z ]v]v ⦄ › proof(rule wfG_wfT)    
        show ‹ Θ ; ℬ  ⊢wf (x, B_bool, c[x::=[ z ]v]v[z::=[ x ]v]cv) #Γ Γ › using c check_s_wf assms by metis
        have " atom x ♯ [ z ]v" using v.fresh z fresh_at_base by auto
        thus  ‹atom x ♯ c[x::=[ z ]v]v› using fresh_subst_v_if[of "atom x" c ] by auto
      qed
      have wfg: "Θ ; ℬ ⊢wf(x, B_bool, ([ [ z ]v ]ce  ==  [ [ L_true ]v ]ce )[z::=[ x ]v]v) #Γ Γ" 
        using wfT_wfG vt infer_v_wf fresh_prodN assms by simp
      show  ‹Θ ; ℬ ; (x, B_bool, ([ [ z ]v ]ce  ==  [ [ L_true ]v ]ce )[z::=[ x ]v]v) #Γ Γ  ⊨ c[x::=[ z ]v]v[z::=[ x ]v]v › 
        using c valid_weakening[OF assms(3) _ wfg ] toSet.simps 
        using subst_v_c_def by auto
    qed
    show ‹atom z ♯ (x, [ L_true ]v)› using z fresh_prodN by metis
    show ‹ Θ ; Φ ; ℬ ; (x, B_bool, c) #Γ Γ ; Δ  ⊢ s ⇐ τ› using assms by auto

    thus ‹(x, B_bool, c) #Γ Γ = GNil @ (x, B_bool, c[x::=[ z ]v]v[z::=[ x ]v]cv) #Γ Γ› using append_g.simps c by auto
  qed

  moreover have "((x,B_bool, c) #Γ Γ)[x::=?v]Γv = Γ " using subst_gv.simps by auto
  ultimately show ?thesis using assms forget_subst_dv forget_subst_sv forget_subst_tv fresh_prodN  by metis
qed

lemma check_assert_s:
  fixes s::s and x::x
  assumes "Θ; Φ; {||}; GNil; Δ  ⊢  AS_assert c s  ⇐ τ"
  shows "Θ; Φ; {||}; GNil; Δ  ⊢  s  ⇐ τ ∧ Θ ; {||} ; GNil  ⊨ c "
proof -
  let ?B = "({||}::bv fset)"
  let ?v = "V_lit L_true"

  obtain x where x: "Θ ; Φ ; ?B ; (x,B_bool, c) #Γ GNil ; Δ  ⊢  s  ⇐ τ ∧ atom x ♯ (Θ, Φ, ?B, GNil, Δ, c, τ, s ) ∧ Θ ; ?B ; GNil ⊨ c " 
    using check_s_elims(10)[OF ‹Θ ; Φ ; ?B ; GNil ; Δ  ⊢  AS_assert c s   ⇐ τ›] valid.simps by metis

  show ?thesis using assms check_s_narrow x by metis
qed

lemma infer_v_pair2I:
  "atom z ♯ (v1, v2) ⟹
   atom z ♯ (Θ, ℬ, Γ) ⟹
   Θ ; ℬ ; Γ ⊢ v1 ⇒ t1 ⟹
   Θ ; ℬ ; Γ ⊢ v2 ⇒ t2 ⟹
   b1 = b_of t1 ⟹ b2 = b_of t2 ⟹ 
  Θ ; ℬ ; Γ ⊢ [ v1 , v2 ]v ⇒ ⦃ z : [ b1 , b2 ]b  | [ [ z ]v ]ce  ==  [ [ v1 , v2 ]v ]ce  ⦄"
  using infer_v_pairI by simp

subsection ‹Main Lemma›

lemma preservation: 
  assumes "Φ ⊢ ⟨δ, s⟩ ⟶ ⟨δ', s'⟩" and "Θ; Φ; Δ ⊢ ⟨δ, s⟩ ⇐ τ"
  shows "∃Δ'. Θ; Φ; Δ' ⊢ ⟨δ', s'⟩ ⇐ τ ∧ Δ ⊑ Δ'" 
  using assms 
proof(induct arbitrary: τ rule: reduce_stmt.induct)
  case (reduce_let_plusI δ x n1 n2 s')
  then show ?case using preservation_plus
    by (metis order_refl)  
next
  case (reduce_let_leqI b n1 n2 δ x s) 
  then show ?case using preservation_leq  by (metis order_refl)  
next
  case (reduce_let_eqI b n1 n2 Φ δ x s)
  then show ?case using preservation_eq[OF reduce_let_eqI(2)] order_refl by metis
next
  case (reduce_let_appI f z b c τ' s' Φ δ x v s)
  hence tt: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_app f v) s ⇐ τ ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" using config_type_elims[OF reduce_let_appI(2)] by metis 
  hence *:"Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_app f v) s ⇐ τ" by auto

  hence  "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let2 x   (τ'[z::=v]τv) (s'[z::=v]sv) s ⇐ τ" 
    using preservation_app reduce_let_appI tt by auto

  hence "Θ; Φ; Δ ⊢ ⟨ δ , AS_let2 x (τ'[z::=v]τv) s'[z::=v]sv s ⟩ ⇐ τ"  using  config_typeI tt by auto
  then show ?case using tt order_refl reduce_let_appI by metis

next
  case (reduce_let_appPI f bv z b c τ' s' Φ δ x b' v s)

  hence tt: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_appP f b' v) s ⇐ τ ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" using config_type_elims[OF reduce_let_appPI(2)] by metis 
  hence *:"Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_appP f b' v) s ⇐ τ" by auto

  have  "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let2 x   (τ'[bv::=b']τb[z::=v]τv) (s'[bv::=b']sb[z::=v]sv) s ⇐ τ" 
  proof(rule preservation_poly_app) 
    show ‹Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ z b c  τ' s'))) = lookup_fun Φ f› using reduce_let_appPI by metis
    show ‹∀fd∈set Φ. check_fundef Θ Φ fd› using tt lookup_fun_member by metis
    show ‹ Θ ; Φ ;{||} ; GNil ; Δ  ⊢ AS_let x (AE_appP f b' v) s ⇐ τ› using * by auto
    show ‹ Θ ; {||}  ⊢wf b' › using check_s_elims infer_e_wf wfE_elims * by metis
  qed(auto+)

  hence "Θ; Φ; Δ ⊢ ⟨ δ , AS_let2 x (τ'[bv::=b']τb[z::=v]τv) s'[bv::=b']sb[z::=v]sv s ⟩ ⇐ τ"  using  config_typeI tt by auto
  then show ?case using tt order_refl reduce_let_appI by metis

next
  case (reduce_if_trueI δ s1 s2) 
  then show ?case using preservation_if by metis
next
  case (reduce_if_falseI uw δ s1 s2)
  then show ?case using preservation_if by metis
next
  case (reduce_let_valI δ x v s)
  then show ?case using preservation_let_val by presburger
next
  case (reduce_let_mvar u v δ Φ  x s)
  hence *:"Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_mvar u) s ⇐ τ ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by blast

  hence **: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_mvar u) s ⇐ τ" by auto
  obtain xa::x and za::x and ca::c and ba::b and sa::s where
    sa1: "atom xa ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, AE_mvar u, τ) ∧  atom za ♯ (xa, Θ, Φ, {||}::bv fset, GNil, Δ, AE_mvar u, τ, sa) ∧
     Θ; Φ; {||}; GNil; Δ   ⊢ AE_mvar u ⇒ ⦃ za : ba  | ca ⦄ ∧
     Θ ; Φ ; {||} ; (xa, ba, ca[za::=V_var xa]cv) #Γ GNil ; Δ   ⊢ sa ⇐ τ ∧
       (∀c. atom c ♯ (s, sa) ⟶ atom c ♯ (x, xa, s, sa) ⟶ (x ↔ c) ∙ s = (xa ↔ c) ∙ sa)" 
    using check_s_elims(2)[OF **] subst_defs by metis

  have "Θ ; {||} ; GNil ⊢ v ⇐  ⦃ za : ba  | ca ⦄" proof -
    have " (u , ⦃ za : ba  | ca ⦄) ∈ setD Δ" using infer_e_elims(11) sa1 by fast
    thus  ?thesis using delta_sim_v reduce_let_mvar config_type_elims check_s_wf  by metis
  qed

  then obtain τ' where  vst: "Θ ; {||} ; GNil ⊢ v ⇒ τ' ∧
        Θ ; {||} ; GNil ⊢ τ'  ≲  ⦃ za : ba  | ca ⦄" using check_v_elims by blast

  obtain za2 and ba2 and ca2 where  zbc: "τ' = (⦃ za2 : ba2 | ca2 ⦄) ∧ atom za2 ♯ (xa, (xa, Θ, Φ, {||}::bv fset, GNil, Δ, AE_val v, τ, sa))"
    using obtain_fresh_z by blast
  have beq: "ba=ba2" using subtype_eq_base vst zbc by blast

  moreover have xaf: "atom xa ♯ (za, za2)" 
    apply(unfold fresh_prodN, intro conjI)
    using sa1 zbc fresh_prodN fresh_x_neq by metis+

  have sat2: " Θ ; Φ ; {||} ; GNil@(xa, ba, ca2[za2::=V_var xa]cv) #Γ GNil ; Δ   ⊢ sa ⇐ τ" proof(rule ctx_subtype_s)
    show "Θ ; Φ ; {||} ; GNil @ (xa, ba, ca[za::=V_var xa]cv) #Γ GNil ; Δ  ⊢ sa ⇐ τ" using sa1 by auto
    show "Θ ; {||} ; GNil  ⊢ ⦃ za2 : ba  | ca2 ⦄ ≲ ⦃ za : ba  | ca ⦄" using beq zbc vst by fast
    show "atom xa ♯ (za, za2, ca, ca2)" proof -
      have *:"Θ ; {||} ; GNil ⊢wf (⦃ za2 : ba2 | ca2 ⦄) " using zbc vst subtype_wf by auto
      hence "supp ca2 ⊆ { atom za2 }" using wfT_supp_c[OF *] supp_GNil by simp
      moreover have "atom za2 ♯ xa" using zbc fresh_Pair fresh_x_neq by metis
      ultimately have  "atom xa ♯ ca2" using zbc supp_at_base fresh_def 
        by (metis empty_iff singleton_iff subset_singletonD)
      moreover have "atom xa ♯ ca" proof -
        have *:"Θ ; {||} ; GNil ⊢wf (⦃ za : ba | ca ⦄) " using zbc vst subtype_wf by auto
        hence "supp ca ⊆ { atom za }" using wfT_supp τ.supp by force
        moreover have "xa ≠ za"  using   fresh_def fresh_x_neq xaf fresh_Pair by metis
        ultimately show ?thesis using fresh_def by auto
      qed
      ultimately show ?thesis using xaf sa1 fresh_prod4 fresh_Pair by metis
    qed
  qed
  hence dwf: "Θ ; {||} ; GNil  ⊢wf Δ" using sa1 infer_e_wf by meson

  have "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let xa (AE_val v) sa ⇐ τ" proof 
    have "atom xa ♯ (AE_val v)" using infer_v_wf(1) wfV_supp fresh_def e.fresh x_not_in_b_set vst by fastforce
    thus  "atom xa ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, AE_val v, τ)" using sa1 freshers by simp 
    have "atom za2 ♯ (AE_val v)" using infer_v_wf(1) wfV_supp fresh_def e.fresh x_not_in_b_set vst by fastforce
    thus "atom za2 ♯ (xa, Θ, Φ, {||}::bv fset, GNil, Δ, AE_val v, τ, sa)" using zbc freshers fresh_prodN by auto
    have " Θ    ⊢wf Φ" using sa1 infer_e_wf by auto
    thus  "Θ; Φ; {||}; GNil; Δ   ⊢ AE_val v ⇒ ⦃ za2 : ba  | ca2 ⦄" 
      using zbc vst beq dwf infer_e_valI by blast
    show "Θ ; Φ ; {||} ; (xa, ba, ca2[za2::=V_var xa]v) #Γ GNil ; Δ   ⊢ sa ⇐ τ" using sat2 append_g.simps subst_defs by metis
  qed
  moreover have  "AS_let xa (AE_val v) sa =  AS_let x (AE_val v) s" proof -
    have "[[atom x]]lst. s = [[atom xa]]lst. sa" 
      using sa1 Abs1_eq_iff_all(3)[where z=" (s, sa)"] by metis
    thus ?thesis using s_branch_s_branch_list.eq_iff(2) by metis
  qed
  ultimately have "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let x (AE_val v) s ⇐ τ"  by auto

  then show ?case using reduce_let_mvar * config_typeI
    by (meson order_refl)
next
  case (reduce_let2I Φ δ s1 δ' s1'  x t s2)
  hence **: "Θ; Φ; {||}; GNil; Δ   ⊢ AS_let2 x t s1 s2  ⇐ τ  ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" using config_type_elims[OF reduce_let2I(3)] by blast
  hence *:"Θ; Φ; {||}; GNil; Δ   ⊢ AS_let2 x t s1 s2  ⇐ τ" by auto

  obtain xa::x and  z::x and c and b and s2a::s where st: "atom xa ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, t, s1, τ)  ∧
       Θ; Φ; {||}; GNil; Δ   ⊢ s1 ⇐ t ∧
       Θ ; Φ ; {||} ; (xa, b_of t, c_of t xa) #Γ GNil ; Δ   ⊢ s2a ⇐ τ ∧  ([[atom x]]lst. s2 = [[atom xa]]lst. s2a) "
    using check_s_elims(4)[OF *] Abs1_eq_iff_all(3) by metis

  hence "Θ; Φ; Δ ⊢ ⟨ δ , s1 ⟩ ⇐ t"  using config_typeI ** by auto
  then obtain Δ' where s1r: "Θ; Φ; Δ' ⊢ ⟨ δ' , s1' ⟩ ⇐ t ∧ Δ ⊑ Δ'" using reduce_let2I by presburger

  have  "Θ; Φ; {||}; GNil; Δ'  ⊢ AS_let2 xa t s1' s2a  ⇐ τ" 
  proof(rule check_let2I)
    show *:"Θ; Φ; {||}; GNil; Δ'  ⊢ s1' ⇐ t" using config_type_elims st s1r by metis
    show  "atom xa ♯ (Θ, Φ, {||}::bv fset, GNil, Δ',t, s1', τ)" proof -  
      have "atom xa ♯ s1'" using  check_s_x_fresh *  by auto
      moreover have "atom xa ♯ Δ'" using check_s_x_fresh * by auto
      ultimately show ?thesis  using st fresh_prodN by metis
    qed

    show "Θ ; Φ ; {||} ; (xa, b_of t, c_of t xa) #Γ GNil ; Δ'  ⊢ s2a ⇐ τ"  proof -
      have "Θ ; {||} ; GNil  ⊢wf Δ'" using * check_s_wf by auto
      moreover have "Θ ; {||} ⊢wf ((xa, b_of t, c_of t xa) #Γ GNil)" using st check_s_wf by auto
      ultimately have "Θ ; {||} ; ((xa, b_of t , c_of t xa) #Γ GNil)  ⊢wf Δ'" using wf_weakening by auto
      thus  ?thesis using check_s_d_weakening check_s_wf st  s1r by metis
    qed
  qed
  moreover have "AS_let2 xa t s1' s2a = AS_let2 x t s1' s2"  using st s_branch_s_branch_list.eq_iff by metis
  ultimately have "Θ; Φ; {||}; GNil; Δ'  ⊢ AS_let2 x t s1' s2  ⇐ τ" using st by argo
  moreover have "Θ ⊢ δ' ∼ Δ'" using config_type_elims s1r by fast
  ultimately show ?case using config_typeI **
    by (meson s1r)
next
  case (reduce_let2_valI vb δ x t v s)
  then show ?case using preservation_let_val by meson
next
  case (reduce_varI u δ Φ τ' v s)

  hence ** : "Θ; Φ; {||}; GNil; Δ  ⊢ AS_var u τ' v s ⇐ τ ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by meson
  have uf: "atom u ♯ Δ" using reduce_varI delta_sim_fresh by force  
  hence *: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_var u τ' v s ⇐ τ" and " Θ ⊢ δ ∼ Δ" using **  by auto

  thus ?case using preservation_var reduce_varI config_typeI ** set_subset_Cons
      setD_ConsD subsetI  by (metis delta_sim_fresh)

next
  case (reduce_assignI Φ δ u v )
  hence *: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_assign u v  ⇐ τ ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by meson
  then obtain z and τ' where zt: "Θ ; {||} ; GNil ⊢ (⦃ z : B_unit | TRUE ⦄) ≲ τ ∧ (u,τ') ∈ setD Δ ∧ Θ ; {||} ; GNil ⊢ v ⇐ τ' ∧ Θ ; {||} ; GNil  ⊢wf Δ" 
    using check_s_elims(8) by metis
  hence "Θ ⊢ update_d δ u v ∼ Δ" using update_d_sim  * by metis
  moreover have "Θ; Φ; {||}; GNil; Δ  ⊢ AS_val (V_lit L_unit ) ⇐ τ" using zt * check_s_v_unit check_s_wf
    by auto
  ultimately show ?case using config_typeI * by (meson order_refl)
next
  case (reduce_seq1I Φ δ s)
  hence "Θ ; Φ ;   {||} ; GNil ; Δ ⊢ s ⇐ τ ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using check_s_elims config_type_elims by force
  then show ?case  using config_typeI by blast
next
  case (reduce_seq2I s1 v Φ δ δ' s1' s2)
  hence tt: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_seq s1 s2 ⇐ τ ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by blast
  then obtain z where zz: "Θ ; Φ ; {||} ; GNil; Δ  ⊢ s1 ⇐ (⦃ z : B_unit | TRUE ⦄) ∧  Θ; Φ; {||}; GNil; Δ   ⊢ s2 ⇐ τ" 
    using check_s_elims by blast
  hence "Θ; Φ; Δ ⊢ ⟨ δ , s1 ⟩ ⇐ (⦃ z : B_unit | TRUE ⦄)" 
    using tt config_typeI tt by simp 
  then obtain Δ' where *: "Θ; Φ; Δ' ⊢ ⟨ δ' , s1' ⟩ ⇐ (⦃ z : B_unit | TRUE ⦄) ∧ Δ ⊑ Δ'" 
    using reduce_seq2I by meson
  moreover hence  s't: "Θ; Φ; {||}; GNil; Δ'  ⊢ s1' ⇐ (⦃ z : B_unit | TRUE ⦄) ∧ Θ ⊢ δ' ∼ Δ'" 
    using config_type_elims by force
  moreover hence "Θ ; {||} ; GNil  ⊢wf Δ'" using check_s_wf by meson
  moreover hence  "Θ; Φ; {||}; GNil; Δ'  ⊢ s2 ⇐ τ" 
    using calculation(1) zz check_s_d_weakening * by metis
  moreover hence  "Θ; Φ; {||}; GNil; Δ'  ⊢ (AS_seq s1' s2) ⇐ τ" 
    using check_seqI zz s't by meson 
  ultimately have  "Θ; Φ; Δ'  ⊢ ⟨ δ' , AS_seq s1' s2 ⟩ ⇐ τ ∧ Δ ⊑ Δ'"
    using zz config_typeI tt  by meson
  then show ?case by meson
next
  case (reduce_whileI x  s1 s2 z' Φ δ )

  hence *: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_while s1 s2  ⇐ τ ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by meson

  hence  **:"Θ; Φ; {||}; GNil; Δ  ⊢ AS_while s1 s2  ⇐ τ" by auto
  hence "Θ; Φ; {||}; GNil; Δ  ⊢ AS_let2 x (⦃ z' : B_bool  | TRUE ⦄) s1 (AS_if (V_var x) (AS_seq s2 (AS_while s1 s2))  (AS_val (V_lit L_unit)) ) ⇐ τ"
    using check_while reduce_whileI by auto
  thus ?case  using config_typeI *   by (meson subset_refl)

next
  case (reduce_caseI dc x' s' css Φ δ tyid  v)

  hence **: "Θ; Φ; {||}; GNil; Δ   ⊢ AS_match (V_cons tyid dc v) css ⇐ τ ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)"
    using config_type_elims[OF reduce_caseI(2)] by metis
  hence ***: "Θ; Φ; {||}; GNil; Δ  ⊢ AS_match (V_cons tyid  dc v) css ⇐ τ" by auto

  let ?vcons = "V_cons tyid dc v"

  obtain dclist tid  and z::x where cv:  "Θ; {||} ; GNil ⊢ (V_cons tyid dc v) ⇐ (⦃ z : B_id tid | TRUE ⦄) ∧ 
    Θ; Φ; {||}; GNil; Δ ; tid ; dclist ; (V_cons tyid dc v) ⊢ css ⇐ τ ∧  AF_typedef tid dclist ∈ set Θ ∧ 
 Θ ; {||} ; GNil  ⊢ V_cons tyid dc v ⇐ ⦃ z : B_id tid  | TRUE ⦄"
    using check_s_elims(9)[OF ***] by metis

  hence vi:" Θ ; {||} ; GNil  ⊢ V_cons tyid dc v ⇐ ⦃ z : B_id tid  | TRUE ⦄" by auto
  obtain tcons where vi2:" Θ ; {||} ; GNil  ⊢ V_cons tyid dc v ⇒ tcons ∧ Θ ; {||} ; GNil  ⊢ tcons ≲  ⦃ z : B_id tid  | TRUE ⦄" 
    using check_v_elims(1)[OF vi] by metis
  hence vi1: "Θ ; {||} ; GNil  ⊢ V_cons tyid dc v ⇒ tcons" by auto

  show ?case proof(rule infer_v_elims(4)[OF vi1],goal_cases)
    case (1 dclist2 tc tv z2)
    have "tyid = tid" using τ.eq_iff using subtype_eq_base vi2 1 by fastforce 
    hence deq:"dclist = dclist2"  using check_v_wf wfX_wfY cv 1  wfTh_dclist_unique by metis
    have "Θ; Φ; {||}; GNil; Δ  ⊢ s'[x'::=v]sv ⇐ τ" proof(rule check_match(3))     
      show ‹ Θ ;  Φ ;  {||} ; GNil ; Δ ; tyid ; dclist ; ?vcons ⊢ css ⇐ τ› using ‹tyid = tid› cv by auto
      show "distinct (map fst dclist)" using wfTh_dclist_distinct check_v_wf wfX_wfY cv by metis
      show ‹?vcons = V_cons tyid dc v› by auto
      show ‹{||} = {||}› by auto
      show ‹(dc, tc) ∈ set dclist› using 1 deq by auto
      show ‹GNil = GNil› by auto
      show ‹Some (AS_branch dc x' s') = lookup_branch dc css› using reduce_caseI by auto
      show ‹Θ ; {||} ; GNil  ⊢ v ⇐ tc› using 1 check_v.intros by auto
    qed
    thus  ?case using config_typeI ** by blast
  qed

next
  case (reduce_let_fstI Φ δ x v1 v2 s)
  thus ?case using preservation_fst_snd order_refl by metis
next
  case (reduce_let_sndI  Φ δ x v1 v2 s)
  thus ?case using preservation_fst_snd order_refl by metis
next
  case (reduce_let_concatI Φ δ x v1 v2 s)
  hence elim: "Θ; Φ; {||}; GNil; Δ  ⊢  AS_let x (AE_concat (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))) s ⇐ τ ∧ 
                  Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by metis

  obtain z::x where z: "atom z ♯ (AE_concat (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2)), GNil, CE_val (V_lit (L_bitvec (v1 @ v2))))" 
    using obtain_fresh by metis

  have "Θ ; {||} ⊢wf GNil" using check_s_wf elim by auto

  have "Θ; Φ; {||}; GNil; Δ ⊢ AS_let x (AE_val (V_lit (L_bitvec (v1 @ v2)))) s ⇐ τ" proof(rule subtype_let)
    show ‹ Θ; Φ; {||}; GNil; Δ   ⊢ AS_let x (AE_concat (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))) s ⇐ τ› using elim by auto
    show ‹Θ; Φ; {||}; GNil; Δ   ⊢ (AE_concat (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))) ⇒ ⦃ z : B_bitvec  | CE_val (V_var z)  == (CE_concat ([V_lit (L_bitvec v1)]ce) ([V_lit (L_bitvec v2)]ce))⦄ › 
      (is "Θ; Φ; {||}; GNil; Δ   ⊢ ?e1 ⇒ ?t1")
    proof
      show ‹ Θ ; {||} ; GNil  ⊢wf Δ › using check_s_wf elim by auto
      show ‹ Θ  ⊢wf Φ › using check_s_wf elim by auto
      show ‹ Θ ; {||} ; GNil  ⊢ V_lit (L_bitvec v1) ⇒ ⦃ z : B_bitvec | CE_val (V_var z) == CE_val (V_lit (L_bitvec v1)) ⦄› 
        using infer_v_litI infer_l.intros  ‹Θ ; {||} ⊢wf GNil›  fresh_GNil by auto
      show ‹ Θ ; {||} ; GNil  ⊢ V_lit (L_bitvec v2) ⇒ ⦃ z : B_bitvec | CE_val (V_var z) == CE_val (V_lit (L_bitvec v2)) ⦄› 
        using infer_v_litI infer_l.intros  ‹Θ ; {||} ⊢wf GNil›  fresh_GNil by auto
      show ‹atom z ♯ AE_concat (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))› using z fresh_Pair by metis
      show ‹atom z ♯ GNil› using z fresh_Pair by auto
    qed
    show ‹Θ; Φ; {||}; GNil; Δ   ⊢ AE_val (V_lit (L_bitvec (v1 @ v2))) ⇒  ⦃ z : B_bitvec  | CE_val (V_var z) == CE_val (V_lit (L_bitvec (v1 @ v2))) ⦄ › 
      (is "Θ; Φ; {||}; GNil; Δ   ⊢ ?e2 ⇒ ?t2")
      using infer_e_valI infer_v_litI infer_l.intros  ‹Θ ; {||} ⊢wf GNil›  fresh_GNil check_s_wf elim by metis
    show ‹Θ ; {||} ; GNil  ⊢ ?t2 ≲ ?t1› using subtype_concat check_s_wf elim by auto
  qed

  thus ?case  using config_typeI elim by (meson order_refl)
next
  case (reduce_let_lenI Φ δ x v s)
  hence elim: "Θ; Φ; {||}; GNil; Δ  ⊢  AS_let x (AE_len (V_lit (L_bitvec v))) s ⇐ τ ∧ Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using check_s_elims config_type_elims by metis

  then obtain t where t: "Θ; Φ; {||}; GNil; Δ  ⊢ AE_len (V_lit (L_bitvec v)) ⇒ t"   using check_s_elims by meson

  moreover then obtain z::x where  "t = ⦃ z : B_int  | CE_val (V_var z)  ==  CE_len ([V_lit (L_bitvec v)]ce)  ⦄" using infer_e_elims by meson 

  moreover obtain z'::x where "atom z' ♯ v" using obtain_fresh by metis
  moreover have  "Θ; Φ; {||}; GNil; Δ ⊢  AE_val (V_lit (L_num (int (length v)))) ⇒ ⦃ z' : B_int  | CE_val (V_var z')  ==  CE_val (V_lit (L_num (int (length v))))  ⦄" 
    using infer_e_valI infer_v_litI infer_l.intros(3)  t  check_s_wf elim 
    by (metis infer_l_form2 type_for_lit.simps(3))

  moreover have "Θ ; {||} ; GNil ⊢   ⦃ z' : B_int  | CE_val (V_var z')  ==  CE_val (V_lit (L_num (int (length v))))  ⦄ ≲ 
                           ⦃ z : B_int  | CE_val (V_var z)  ==  CE_len [(V_lit (L_bitvec v))]ce  ⦄" using subtype_len check_s_wf elim by auto

  ultimately have "Θ; Φ; {||}; GNil; Δ ⊢  AS_let x (AE_val (V_lit (L_num (int (length v)))))  s ⇐ τ" using subtype_let by (meson elim)
  thus ?case  using config_typeI elim by (meson order_refl)
next
  case (reduce_let_splitI n v v1 v2 Φ δ x s)
  hence elim: "Θ; Φ; {||}; GNil; Δ  ⊢  AS_let x (AE_split (V_lit (L_bitvec v)) (V_lit (L_num n))) s ⇐ τ ∧ 
                  Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by metis

  obtain z::x where z: "atom z ♯ (AE_split (V_lit (L_bitvec v)) (V_lit (L_num n)), GNil, CE_val (V_lit (L_bitvec (v1 @ v2))), 
([ L_bitvec v1 ]v, [ L_bitvec v2 ]v), Θ, {||}::bv fset)" 
    using obtain_fresh by metis

  have *:"Θ ; {||} ⊢wf GNil" using check_s_wf elim by auto

  have "Θ; Φ; {||}; GNil; Δ ⊢ AS_let x (AE_val (V_pair (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2)))) s ⇐ τ" proof(rule subtype_let)

    show ‹ Θ; Φ; {||}; GNil; Δ   ⊢ AS_let x (AE_split (V_lit (L_bitvec v)) (V_lit (L_num n))) s ⇐ τ› using elim by auto
    show ‹Θ; Φ; {||}; GNil; Δ   ⊢ (AE_split (V_lit (L_bitvec v)) (V_lit (L_num n))) ⇒ ⦃ z : B_pair B_bitvec B_bitvec  
                 |   ((CE_val (V_lit (L_bitvec v))) == (CE_concat (CE_fst (CE_val (V_var z))) (CE_snd (CE_val (V_var z)))))
                  AND (((CE_len (CE_fst (CE_val (V_var z))))) == (CE_val (V_lit (L_num n)))) ⦄ › 
      (is "Θ; Φ; {||}; GNil; Δ   ⊢ ?e1 ⇒ ?t1") 
    proof
      show ‹ Θ ; {||} ; GNil  ⊢wf Δ › using check_s_wf elim by auto
      show ‹ Θ  ⊢wf Φ › using check_s_wf elim by auto
      show ‹ Θ ; {||} ; GNil  ⊢ V_lit (L_bitvec v) ⇒ ⦃ z : B_bitvec | CE_val (V_var z) == CE_val (V_lit (L_bitvec v)) ⦄› 
        using infer_v_litI infer_l.intros  ‹Θ ; {||} ⊢wf GNil›  fresh_GNil by auto
      show "Θ ; {||} ; GNil  ⊢ ([ L_num
                           n ]v) ⇐ ⦃ z : B_int  | (([ leq [ [ L_num 0 ]v ]ce [ [ z ]v ]ce ]ce)  ==  ([ [ L_true ]v ]ce))   AND  [ leq [ [ z ]v ]ce [| [ [ L_bitvec
                   v ]v ]ce |]ce ]ce  ==  [ [ L_true ]v ]ce   ⦄" using split_n  reduce_let_splitI check_v_num_leq * wfX_wfY  by metis
      show ‹atom z ♯ AE_split [ L_bitvec v ]v [ L_num n ]v› using z fresh_Pair by auto
      show ‹atom z ♯ GNil› using z fresh_Pair by auto
      show ‹atom z ♯ AE_split [ L_bitvec v ]v [ L_num n ]v› using z fresh_Pair by auto
      show ‹atom z ♯ GNil› using z fresh_Pair by auto
      show ‹atom z ♯ AE_split [ L_bitvec v ]v [ L_num n ]v› using z fresh_Pair by auto
      show ‹atom z ♯ GNil› using z fresh_Pair by auto
    qed

    show ‹Θ; Φ; {||}; GNil; Δ   ⊢ AE_val (V_pair (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))) ⇒  ⦃ z : B_pair B_bitvec  B_bitvec  | CE_val (V_var z) == CE_val ((V_pair (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2)))) ⦄ › 
      (is "Θ; Φ; {||}; GNil; Δ   ⊢ ?e2 ⇒ ?t2")
      apply(rule infer_e_valI)
      using check_s_wf elim apply metis
      using check_s_wf elim apply metis      
      apply(rule infer_v_pair2I)
      using z fresh_prodN apply metis
      using z fresh_GNil fresh_prodN apply metis
      using  infer_v_litI infer_l.intros  ‹Θ ; {||} ⊢wf GNil› b_of.simps  apply blast+
      using b_of.simps apply simp+
      done
    show ‹Θ ; {||} ; GNil  ⊢ ?t2 ≲ ?t1› using subtype_split check_s_wf elim reduce_let_splitI by auto
  qed

  thus ?case  using config_typeI elim by (meson order_refl)
next
  case (reduce_assert1I Φ δ c v)

  hence elim: "Θ; Φ; {||}; GNil; Δ  ⊢  AS_assert c [v]s   ⇐ τ ∧ 
                  Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims reduce_assert1I by metis
  hence *:"Θ; Φ; {||}; GNil; Δ  ⊢  AS_assert c [v]s   ⇐ τ" by auto

  have  "Θ; Φ; {||}; GNil; Δ  ⊢  [v]s   ⇐ τ" using  check_assert_s *  by metis
  thus  ?case using elim config_typeI  by blast
next
  case (reduce_assert2I Φ δ s δ' s' c)

  hence elim: "Θ; Φ; {||}; GNil; Δ  ⊢  AS_assert c s  ⇐ τ ∧ 
                  Θ ⊢ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by metis
  hence *:"Θ; Φ; {||}; GNil; Δ  ⊢  AS_assert c s   ⇐ τ" by auto

  have  cv: "Θ; Φ; {||}; GNil; Δ  ⊢  s   ⇐ τ ∧ Θ ; {||} ; GNil  ⊨ c " using check_assert_s *  by metis

  hence "Θ; Φ; Δ ⊢ ⟨δ, s⟩ ⇐ τ" using elim config_typeI by simp
  then obtain Δ' where D: "Θ; Φ; Δ' ⊢ ⟨ δ' , s' ⟩ ⇐ τ  ∧ Δ ⊑ Δ'" using reduce_assert2I by metis
  hence **:"Θ; Φ; {||}; GNil; Δ' ⊢ s' ⇐ τ ∧ Θ ⊢ δ' ∼ Δ'" using config_type_elims by metis

  obtain x::x where x:"atom x ♯ (Θ, Φ, ({||}::bv fset), GNil, Δ', c, τ, s')" using obtain_fresh by metis

  have *:"Θ; Φ; {||}; GNil; Δ'  ⊢ AS_assert c s'  ⇐ τ" proof
    show "atom x ♯ (Θ, Φ, {||}, GNil, Δ', c, τ, s')" using x by auto
    have "Θ ; {||} ; GNil ⊢wf c" using * check_s_wf by auto
    hence wfg:"Θ ; {||} ⊢wf (x, B_bool, c) #Γ GNil" using wfC_wfG wfB_boolI check_s_wf *  fresh_GNil by auto
    moreover have cs: "Θ; Φ; {||}; GNil; Δ' ⊢ s' ⇐ τ" using ** by auto
    ultimately show  "Θ ; Φ ; {||} ; (x, B_bool, c) #Γ GNil ; Δ'  ⊢ s' ⇐ τ" using check_s_g_weakening(1)[OF cs _ wfg]   toSet.simps  by simp
    show "Θ ; {||} ; GNil  ⊨ c " using cv by auto
    show "Θ ; {||} ; GNil ⊢wf Δ' " using check_s_wf ** by auto
  qed

  thus  ?case using elim config_typeI D ** by metis
qed

lemma preservation_many: 
  assumes " Φ  ⊢ ⟨δ, s⟩ ⟶* ⟨ δ' , s' ⟩"
  shows "Θ; Φ; Δ ⊢  ⟨δ, s⟩ ⇐ τ ⟹ ∃Δ'. Θ; Φ; Δ' ⊢ ⟨ δ' , s' ⟩ ⇐ τ ∧ Δ ⊑ Δ'" 
  using assms proof(induct arbitrary: Δ rule: reduce_stmt_many.induct)
  case (reduce_stmt_many_oneI Φ δ s δ' s')
  then show ?case using preservation by simp
next
  case (reduce_stmt_many_manyI Φ δ s δ' s' δ'' s'')
  then show ?case using preservation subset_trans by metis
qed

section ‹Progress›
text ‹We prove that a well typed program is either a value or we can make a step›

lemma check_let_op_infer:
  assumes  "Θ; Φ; {||}; Γ; Δ   ⊢ LET x = (AE_op opp v1 v2) IN s ⇐ τ" and "supp ( LET x = (AE_op opp v1 v2) IN s) ⊆ atom`fst`setD Δ"
  shows  "∃ z b c. Θ; Φ; {||}; Γ; Δ ⊢  (AE_op opp v1 v2) ⇒ ⦃z:b|c⦄"
proof - 
  have xx: "Θ; Φ; {||}; Γ; Δ ⊢ LET x = (AE_op opp v1 v2) IN s ⇐ τ" using assms by simp
  then show ?thesis using check_s_elims(2)[OF xx] by meson
qed

lemma infer_pair:
  assumes "Θ ; B; Γ ⊢  v  ⇒ ⦃ z : B_pair b1 b2  | c ⦄" and "supp v = {}"
  obtains v1 and v2 where "v = V_pair v1 v2" 
  using assms proof(nominal_induct v rule: v.strong_induct)
  case (V_lit x)
  then show ?case by auto
next
  case (V_var x)
  then show ?case using v.supp supp_at_base by auto
next
  case (V_pair x1a x2a)
  then show ?case by auto
next
  case (V_cons x1a x2a x3)
  then show ?case by auto
next
  case (V_consp x1a x2a x3 x4)
  then show ?case by auto
qed

lemma progress_fst:
  assumes  "Θ; Φ; {||}; Γ; Δ  ⊢ LET x = (AE_fst v) IN s ⇐ τ" and  "Θ ⊢ δ ∼ Δ" and 
    "supp (LET x = (AE_fst v) IN s)  ⊆ atom`fst`setD Δ"
  shows "∃δ' s'. Φ  ⊢ ⟨ δ , LET x = (AE_fst v) IN s ⟩ ⟶ ⟨δ', s'⟩"
proof -
  have *:"supp v = {}" using assms s_branch_s_branch_list.supp by auto
  obtain z and b and c where "Θ; Φ; {||}; Γ; Δ ⊢  (AE_fst v ) ⇒ ⦃ z : b  | c ⦄" 
    using check_s_elims(2)  using assms by meson
  moreover obtain z' and b' and c' where "Θ ; {||} ; Γ ⊢  v  ⇒ ⦃ z' : B_pair b b'  | c' ⦄" 
    using infer_e_elims(8)  using calculation by auto 
  moreover then obtain v1 and v2 where "V_pair v1 v2 = v" 
    using * infer_pair by metis
  ultimately show ?thesis using reduce_let_fstI assms  by metis
qed

lemma progress_let:
  assumes "Θ; Φ; {||}; Γ; Δ ⊢ LET x = e IN s ⇐ τ" and "Θ ⊢ δ ∼ Δ" and 
    "supp (LET x = e IN s) ⊆ atom ` fst ` setD Δ" and "sble Θ Γ"
  shows "∃δ' s'. Φ  ⊢ ⟨ δ , LET x = e IN s⟩ ⟶ ⟨ δ' , s'⟩"
proof -
  obtain z b c where *: "Θ; Φ; {||}; Γ; Δ  ⊢ e ⇒ ⦃ z : b  | c ⦄ " using check_s_elims(2)[OF assms(1)] by metis
  have **: "supp e ⊆ atom ` fst ` setD Δ" using assms s_branch_s_branch_list.supp by auto
  from * ** assms show ?thesis proof(nominal_induct "⦃ z : b  | c ⦄"  rule: infer_e.strong_induct)
    case (infer_e_valI Θ ℬ Γ Δ Φ v)
    then show ?case using reduce_stmt_elims reduce_let_valI by metis
  next
    case (infer_e_plusI Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
    hence vf: "supp v1 = {} ∧ supp v2 = {}"  by force
    then obtain n1 and n2 where *: "v1 = V_lit (L_num n1)  ∧ v2 = (V_lit (L_num n2))" using infer_int infer_e_plusI by metis
    then show ?case using reduce_let_plusI * by metis
  next
    case (infer_e_leqI Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
    hence vf: "supp v1 = {} ∧ supp v2 = {}"  by force
    then obtain n1 and n2 where *: "v1 = V_lit (L_num n1)  ∧ v2 = (V_lit (L_num n2))" using infer_int infer_e_leqI by metis
    then show ?case using reduce_let_leqI * by metis
  next
    case (infer_e_eqI Θ ℬ Γ Δ Φ v1 z1 bb c1 v2 z2 c2 z3)
    hence vf: "supp v1 = {} ∧ supp v2 = {}"  by force
    then obtain n1 and n2 where *: "v1 = V_lit n1  ∧ v2 = (V_lit n2)" using infer_lit infer_e_eqI by metis
    then show ?case using reduce_let_eqI by blast
  next
    case (infer_e_appI Θ ℬ Γ Δ Φ f x b c τ' s' v)
    then show ?case using reduce_let_appI by metis
  next
    case (infer_e_appPI Θ ℬ Γ Δ Φ b' f bv x b c τ' s' v)
    then show ?case using reduce_let_appPI by metis
  next
    case (infer_e_fstI Θ ℬ Γ Δ Φ v z' b2 c z)
    hence "supp v = {}" by force
    then obtain v1 and v2 where "v = V_pair v1 v2" using infer_e_fstI infer_pair by metis
    then show ?case using reduce_let_fstI * by metis
  next
    case (infer_e_sndI Θ ℬ Γ Δ Φ v z' b1 c z)
    hence "supp v = {}" by force
    then obtain v1 and v2 where "v = V_pair v1 v2" using infer_e_sndI infer_pair by metis
    then show ?case using reduce_let_sndI * by metis
  next
    case (infer_e_lenI Θ ℬ Γ Δ Φ v z' c za)
    hence "supp v = {}" by force
    then obtain bvec where "v = V_lit (L_bitvec bvec)" using infer_e_lenI infer_bitvec by metis
    then show ?case using reduce_let_lenI * by metis
  next
    case (infer_e_mvarI Θ ℬ Γ Φ Δ u)
    hence "(u, ⦃ z : b  | c ⦄) ∈ setD Δ" using infer_e_elims(10) by meson
    then obtain v where "(u,v) ∈ set δ" using infer_e_mvarI delta_sim_delta_lookup by meson
    then show ?case using reduce_let_mvar by metis
  next
    case (infer_e_concatI Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
    hence vf: "supp v1 = {} ∧ supp v2 = {}"  by force
    then obtain n1 and n2 where *: "v1 = V_lit (L_bitvec n1)  ∧ v2 = (V_lit (L_bitvec n2))" using infer_bitvec infer_e_concatI by metis
    then show ?case using reduce_let_concatI * by metis
  next
    case (infer_e_splitI Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 z3)
    hence vf: "supp v1 = {} ∧ supp v2 = {}"  by force
    then obtain n1 and n2 where *: "v1 = V_lit (L_bitvec n1)  ∧ v2 = (V_lit (L_num n2))" using infer_bitvec infer_e_splitI check_int by metis

    have "0 ≤ n2 ∧ n2 ≤ int (length n1)" using  check_v_range[OF _ * ]   infer_e_splitI by simp
    then obtain bv1 and bv2 where "split n2 n1 (bv1 , bv2)" using obtain_split by metis
    then show ?case using reduce_let_splitI * by metis
  qed
qed 

lemma check_css_lookup_branch_exist:
  fixes s::s and cs::branch_s and css::branch_list and v::v
  shows 
    "Θ; Φ; B; G; Δ ⊢  s ⇐ τ ⟹ True" and 
    "check_branch_s Θ Φ  {||} GNil Δ tid dc const v cs τ ⟹ True" and 
    "Θ; Φ; ℬ; Γ; Δ; tid; dclist; v ⊢ css ⇐ τ ⟹ (dc, t) ∈ set dclist ⟹  
              ∃x' s'. Some (AS_branch dc x' s') = lookup_branch dc css"
proof(nominal_induct τ and τ and τ  rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_branch_list_consI Θ Φ ℬ Γ Δ tid cons const v cs τ dclist css)
  then show ?case  using lookup_branch.simps check_branch_list_finalI by force
next
  case (check_branch_list_finalI Θ Φ ℬ Γ Δ tid cons const v cs τ)
  then show ?case  using lookup_branch.simps check_branch_list_finalI by force
qed(auto+)

lemma progress_aux:  
  shows    "Θ; Φ; ℬ; Γ; Δ ⊢ s ⇐ τ ⟹ ℬ = {||} ⟹  sble Θ Γ ⟹ supp s ⊆ atom ` fst ` setD Δ ⟹ Θ ⊢ δ ∼ Δ ⟹ 
               (∃v. s = [v]s) ∨ (∃δ' s'. Φ ⊢ ⟨δ, s⟩ ⟶ ⟨δ', s'⟩)" and
    "Θ; Φ; {||}; Γ; Δ; tid; dc; const; v2 ⊢ cs ⇐ τ  ⟹ supp cs = {} ⟹ True " 
    "Θ; Φ; {||}; Γ; Δ; tid; dclist; v2 ⊢ css ⇐ τ ⟹ supp css = {} ⟹ True " 
proof(induct  rule: check_s_check_branch_s_check_branch_list.inducts)
  case (check_valI Δ Θ Γ v τ' τ)
  then show ?case by auto
next
  case (check_letI x Θ Φ ℬ Γ Δ e τ z s b c)
  hence "Θ; Φ; {||}; Γ; Δ   ⊢   AS_let x e s ⇐ τ" using Typing.check_letI by meson
  then show ?case using progress_let check_letI by metis
next
  case (check_branch_s_branchI Θ ℬ Γ Δ τ const x Φ tid cons v s)
  then show ?case by auto
next
  case (check_branch_list_consI Θ Φ ℬ Γ Δ tid dclist v cs τ css)
  then show ?case by auto
next
  case (check_branch_list_finalI Θ Φ ℬ Γ Δ tid dclist v cs τ)
  then show ?case by auto
next
  case (check_ifI z Θ Φ ℬ Γ Δ v s1 s2 τ)
  have "supp v = {}" using check_ifI s_branch_s_branch_list.supp by auto
  hence "v = V_lit L_true ∨ v = V_lit L_false" using  check_bool_options check_ifI by auto
  then show ?case using reduce_if_falseI reduce_if_trueI check_ifI by meson
next
  case (check_let2I x Θ Φ ℬ G Δ t s1 τ s2 )
  then consider  " (∃v. s1 = AS_val v)" | "(∃δ' a. Φ  ⊢ ⟨δ, s1⟩ ⟶ ⟨δ', a⟩)" by auto
  then show ?case proof(cases)
    case 1
    then show ?thesis using reduce_let2_valI by fast
  next
    case 2
    then show ?thesis using reduce_let2I check_let2I by meson
  qed
next
  case (check_varI u Θ Φ ℬ Γ Δ τ' v τ s)

  obtain uu::u where uf: "atom uu ♯ (u,δ,s) " using obtain_fresh by blast
  obtain sa where " (uu ↔ u ) ∙ s = sa" by presburger
  moreover have "atom uu ♯ s" using uf fresh_prod3 by auto
  ultimately have "AS_var uu τ' v sa = AS_var u τ' v s" using s_branch_s_branch_list.eq_iff(7) Abs1_eq_iff(3)[of uu sa u s] by auto

  moreover have "atom uu ♯ δ" using uf fresh_prod3 by auto
  ultimately have "Φ ⊢ ⟨δ, AS_var u τ' v s⟩ ⟶ ⟨(uu, v) # δ, sa⟩"
    using reduce_varI uf by metis
  then show ?case by auto
next
  case (check_assignI Δ u τ P G v z τ')
  then show ?case using reduce_assignI by blast
next
  case (check_whileI Θ Φ ℬ Γ Δ s1 z s2 τ')
  obtain x::x where "atom x ♯ (s1,s2)" using obtain_fresh by metis
  moreover obtain z::x where "atom z ♯ x" using obtain_fresh by metis
  ultimately show ?case using reduce_whileI by fast
next
  case (check_seqI P Φ ℬ G Δ s1 z s2 τ)
  thus  ?case proof(cases "∃v. s1 = AS_val v")
    case True
    then obtain v where v: "s1 = AS_val v" by blast
    hence "supp v = {}" using check_seqI by auto
    have "∃z1 c1. P; ℬ; G ⊢ v ⇒ (⦃ z1 : B_unit | c1 ⦄)" proof - 
      obtain t where t:"P; ℬ; G ⊢ v ⇒ t ∧ P; ℬ ; G ⊢ t ≲ (⦃ z : B_unit | TRUE ⦄)"  
        using v check_seqI(1) check_s_elims(1) by blast
      obtain z1 and b1 and c1 where teq: "t =  (⦃ z1 : b1 | c1 ⦄)" using obtain_fresh_z by meson
      hence "b1 = B_unit" using subtype_eq_base t by meson
      thus ?thesis using t teq by fast
    qed
    then obtain z1 and c1 where "P ; ℬ ; G ⊢ v ⇒ (⦃ z1 : B_unit | c1 ⦄)" by auto
    hence "v = V_lit L_unit" using infer_v_unit_form ‹supp v = {}› by simp
    hence "s1 = AS_val (V_lit L_unit)" using v by auto
    then show ?thesis using check_seqI reduce_seq1I by meson
  next
    case False
    then show ?thesis using check_seqI reduce_seq2I 
      by (metis Un_subset_iff s_branch_s_branch_list.supp(9))
  qed

next
  case (check_caseI Θ Φ ℬ Γ Δ tid dclist v cs τ  z)
  hence "supp v = {}" by auto

  then obtain v' and dc and t::τ where v: "v = V_cons tid dc v' ∧ (dc, t) ∈ set dclist" 
    using  check_v_tid_form check_caseI by metis
  obtain z and b and c where teq: "t = (⦃ z : b | c ⦄)" using obtain_fresh_z by meson

  moreover then obtain x' s' where  "Some (AS_branch dc x' s') = lookup_branch dc cs" using  v teq check_caseI check_css_lookup_branch_exist by metis
  ultimately show ?case using reduce_caseI v check_caseI dc_of.cases by metis
next
  case (check_assertI x Θ Φ ℬ Γ Δ c τ s)
  hence sps: "supp s ⊆ atom ` fst ` setD Δ" by auto
  have "atom x ♯ c " using check_assertI by auto
  have "atom x ♯ Γ" using check_assertI check_s_wf wfG_elims by metis
  have "sble Θ ((x, B_bool, c) #Γ Γ)" proof -
    obtain i' where i':" i' ⊨ Γ  ∧  Θ; Γ ⊢ i'" using check_assertI sble_def by metis
    obtain i::valuation where i:"i = i' ( x ↦ SBool True)" by auto

    have "i ⊨ (x, B_bool, c) #Γ Γ" proof -
      have "i' ⊨ c" using valid.simps i'  check_assertI by metis
      hence "i ⊨ c" using is_satis_weakening_x i ‹atom x ♯ c› by auto
      moreover have "i ⊨ Γ"  using is_satis_g_weakening_x i' i  check_assertI ‹atom x ♯ Γ› by metis
      ultimately show ?thesis   using is_satis_g.simps i by auto
    qed
    moreover have "Θ ; ((x, B_bool, c) #Γ Γ) ⊢ i" proof(rule  wfI_cons)
      show ‹ i' ⊨ Γ › using i' by auto
      show ‹ Θ ; Γ ⊢ i'› using i' by auto
      show ‹i = i'(x ↦ SBool True)› using i by auto
      show ‹ Θ  ⊢ SBool True: B_bool› using wfRCV_BBoolI by auto
      show ‹atom x ♯ Γ› using check_assertI check_s_wf wfG_elims by auto
    qed
    ultimately show  ?thesis using sble_def by auto
  qed
  then consider "(∃v. s = [v]s)" | "(∃δ' a.  Φ  ⊢ ⟨δ, s⟩ ⟶ ⟨ δ', a⟩)" using check_assertI sps by metis
  hence "(∃δ' a.  Φ  ⊢ ⟨δ, ASSERT c IN s⟩ ⟶ ⟨δ', a⟩)" proof(cases)
    case 1
    then show ?thesis using reduce_assert1I by metis
  next
    case 2
    then show ?thesis using reduce_assert2I by metis
  qed  
  thus ?case by auto
qed

lemma progress:
  assumes "Θ; Φ; Δ ⊢ ⟨δ, s⟩ ⇐ τ" 
  shows "(∃v. s = [v]s) ∨ (∃δ' s'. Φ  ⊢ ⟨δ, s⟩ ⟶ ⟨δ', s'⟩)"
proof -
  have "Θ; Φ; {||}; GNil; Δ ⊢ s ⇐ τ" and "Θ ⊢ δ ∼ Δ"
    using config_type_elims[OF assms(1)] by auto+
  moreover hence "supp s ⊆ atom ` fst ` setD Δ" using check_s_wf wfS_supp by fastforce
  moreover have "sble Θ GNil" using sble_def wfI_def is_satis_g.simps by simp
  ultimately show  ?thesis using progress_aux by blast
qed

section ‹Safety›

lemma  safety_stmt:
  assumes "Φ ⊢ ⟨δ, s⟩ ⟶* ⟨δ', s'⟩" and "Θ; Φ; Δ ⊢  ⟨δ, s⟩ ⇐ τ"
  shows  "(∃v. s' = [v]s) ∨ (∃δ'' s''. Φ  ⊢ ⟨δ', s'⟩ ⟶ ⟨δ'', s''⟩)"  
  using preservation_many progress assms  by meson

lemma safety:
  assumes "⊢ ⟨PROG Θ Φ 𝒢 s⟩ ⇐ τ" and  "Φ  ⊢ ⟨δ_of 𝒢, s⟩ ⟶* ⟨δ', s'⟩"
  shows  "(∃v. s' = [v]s) ∨ (∃δ'' s''. Φ  ⊢ ⟨δ', s'⟩ ⟶ ⟨δ'', s''⟩)"   
  using assms config_type_prog_elims safety_stmt by metis

end