Theory ContextSubtypingL

(*<*)
theory ContextSubtypingL
  imports TypingL "HOL-Eisbach.Eisbach_Tools" SubstMethods
begin
  (*>*)

declare freshers[simp del]

chapter ‹Context Subtyping  Lemmas›

text ‹Lemmas allowing us to replace the type of a variable in the context with a subtype
and have the judgement remain valid. Also known as narrowing.›

section ‹Replace or exchange type of variable in a context›

text ‹ Because the G-context is extended by the statements like let, we will need a generalised 
substitution lemma for statements. 
For this we setup a function that replaces in G (rig) for a particular x the constraint for it.
We also define a well-formedness relation for RIGs that ensures that each new constraint 
implies the old one›

nominal_function replace_in_g_many :: "Γ ⇒ (x*c) list ⇒ Γ" where
  "replace_in_g_many G xcs = List.foldr (λ(x,c) G. G[x ⟼ c]) xcs G"
  by(auto,simp add: eqvt_def replace_in_g_many_graph_aux_def)
nominal_termination (eqvt)  by lexicographic_order

inductive replace_in_g_subtyped :: "Θ ⇒ ℬ ⇒ Γ ⇒ (x*c) list ⇒ Γ ⇒ bool" (‹ _ ; _  ⊢ _ ⟨ _ ⟩ ↝ _› [100,50,50] 50) where
  replace_in_g_subtyped_nilI: "Θ; ℬ ⊢ G ⟨ [] ⟩ ↝ G"
| replace_in_g_subtyped_consI:  "⟦ 
       Some (b,c') = lookup G x ; 
        Θ; ℬ; G ⊢⇩w⇩f c ;
       Θ; ℬ; G[x⟼c] ⊨ c' ; 
       Θ; ℬ ⊢ G[x⟼c] ⟨ xcs ⟩ ↝ G'; x ∉ fst ` set xcs ⟧  ⟹ 
       Θ; ℬ ⊢ G ⟨ (x,c)#xcs ⟩ ↝ G'" 
equivariance replace_in_g_subtyped
nominal_inductive replace_in_g_subtyped .

inductive_cases replace_in_g_subtyped_elims[elim!]:
  "Θ; ℬ ⊢ G ⟨ [] ⟩ ↝ G'"
  "Θ; ℬ ⊢ ((x,b,c)#⇩ΓΓ G) ⟨ acs ⟩ ↝ ((x,b,c)#⇩ΓG')"
  "Θ; ℬ ⊢ G' ⟨ (x,c)# acs ⟩ ↝ G"

lemma rigs_atom_dom_eq:
  assumes "Θ; ℬ ⊢ G ⟨ xcs ⟩ ↝ G'"
  shows "atom_dom G = atom_dom G'"
  using assms proof(induct rule: replace_in_g_subtyped.induct)
  case (replace_in_g_subtyped_nilI G)
  then show ?case by simp
next
  case (replace_in_g_subtyped_consI b c' G x Θ ℬ c xcs G')
  then show ?case using rig_dom_eq atom_dom.simps dom.simps by simp
qed

lemma replace_in_g_wfG:
  assumes "Θ; ℬ ⊢ G ⟨ xcs ⟩ ↝ G'" and  "wfG Θ ℬ G "
  shows "wfG Θ ℬ G'"
  using assms proof(induct rule: replace_in_g_subtyped.induct)
  case (replace_in_g_subtyped_nilI Θ G)
  then show ?case by auto
next
  case (replace_in_g_subtyped_consI b c' G x Θ c xcs G')
  then show ?case using valid_g_wf by auto
qed

lemma wfD_rig_single:
  fixes Δ::Δ and x::x and c::c and G::Γ
  assumes "Θ; ℬ; G ⊢⇩w⇩f Δ " and  "wfG Θ ℬ (G[x⟼c])"
  shows "Θ; ℬ; G[x⟼c]  ⊢⇩w⇩f Δ" 
proof(cases "atom x ∈ atom_dom G")
  case False
  hence "(G[x⟼c]) = G" using assms replace_in_g_forget wfX_wfY by metis
  then show ?thesis using assms by auto
next
  case True
  then obtain G1 G2 b c' where *: "G=G1@(x,b,c')#⇩ΓG2" using split_G by fastforce
  hence **: "(G[x⟼c]) = G1@(x,b,c)#⇩ΓG2" using replace_in_g_inside wfD_wf  assms wfD_wf by metis

  hence "wfG Θ ℬ ((x,b,c)#⇩ΓG2)" using wfG_suffix assms by auto
  hence "Θ; ℬ; (x, b, TRUE) #⇩Γ G2  ⊢⇩w⇩f c" using wfG_elim2 by auto

  thus ?thesis using wf_replace_inside1 assms * ** 
    by (simp add: wf_replace_inside2(6))
qed

lemma wfD_rig:
  assumes  "Θ; ℬ ⊢ G ⟨ xcs ⟩ ↝ G'" and "wfD Θ ℬ G Δ" 
  shows "wfD Θ ℬ G' Δ" 
  using assms proof(induct rule: replace_in_g_subtyped.induct)
  case (replace_in_g_subtyped_nilI Θ G)
  then show ?case by auto
next
  case (replace_in_g_subtyped_consI b c' G x Θ c xcs G')
  then show ?case using wfD_rig_single valid.simps wfC_wf by auto
qed

lemma replace_in_g_fresh:
  fixes x::x
  assumes "Θ; ℬ ⊢ Γ ⟨ xcs ⟩ ↝ Γ'" and  "wfG Θ ℬ Γ" and "wfG Θ ℬ Γ'" and "atom x ♯ Γ"
  shows "atom x ♯ Γ'"
  using  wfG_dom_supp assms fresh_def rigs_atom_dom_eq by metis

lemma replace_in_g_fresh1:
  fixes x::x
  assumes "Θ; ℬ ⊢ Γ ⟨ xcs ⟩ ↝ Γ'" and  "wfG Θ ℬ Γ" and "atom x ♯ Γ"
  shows "atom x ♯ Γ'"
proof -
  have  "wfG Θ ℬ Γ'" using  replace_in_g_wfG assms by auto
  thus ?thesis using assms replace_in_g_fresh by metis
qed

text ‹ Wellscoping for an eXchange list›

inductive wsX:: "Γ ⇒ (x*c) list ⇒ bool" where
  wsX_NilI: "wsX G []"
|  wsX_ConsI: "⟦ wsX G xcs ; atom x ∈ atom_dom G ; x ∉ fst ` set xcs ⟧ ⟹ wsX G ((x,c)#xcs)"
equivariance wsX
nominal_inductive wsX .

lemma wsX_if1:
  assumes "wsX G xcs"
  shows "(( atom ` fst ` set xcs) ⊆ atom_dom G) ∧ List.distinct (List.map fst xcs)"
  using assms by(induct rule: wsX.induct,force+ )

lemma wsX_if2:
  assumes  "(( atom ` fst ` set xcs) ⊆ atom_dom G) ∧ List.distinct (List.map fst xcs)"
  shows  "wsX G xcs"
  using assms proof(induct xcs)
  case Nil
  then show ?case using wsX_NilI by fast
next
  case (Cons a xcs)
  then obtain x and c where xc: "a=(x,c)" by force
  have " wsX G xcs" proof -
    have "distinct (map fst xcs)" using Cons by force
    moreover have " atom ` fst ` set xcs ⊆ atom_dom G" using Cons by simp
    ultimately show ?thesis  using Cons by fast
  qed
  moreover have "atom x ∈ atom_dom G" using Cons xc 
    by simp
  moreover have "x ∉ fst ` set xcs" using Cons xc 
    by simp
  ultimately show ?case using wsX_ConsI xc by blast
qed

lemma wsX_iff:
  "wsX G xcs = ((( atom ` fst ` set xcs) ⊆ atom_dom G) ∧ List.distinct (List.map fst xcs))"
  using wsX_if1 wsX_if2 by meson

inductive_cases wsX_elims[elim!]:
  "wsX G []"
  "wsX G ((x,c)#xcs)"

lemma wsX_cons:
  assumes  "wsX Γ xcs" and  "x ∉ fst ` set xcs" 
  shows "wsX ((x, b, c1) #⇩Γ Γ) ((x, c2) # xcs)" 
  using assms proof(induct Γ)
  case GNil
  then show ?case using atom_dom.simps wsX_iff by auto
next
  case (GCons xbc Γ)
  obtain x' and b' and c' where xbc: "xbc = (x',b',c')" using prod_cases3 by blast
  then have "atom ` fst ` set xcs ⊆ atom_dom (xbc #⇩Γ Γ) ∧ distinct (map fst xcs)"
    using GCons.prems(1) wsX_iff by blast
  then have "wsX ((x, b, c1) #⇩Γ xbc #⇩Γ Γ) xcs"
    by (simp add: Un_commute subset_Un_eq wsX_if2) 
  then show ?case   by (simp add: GCons.prems(2) wsX_ConsI) 
qed

lemma wsX_cons2:
  assumes  "wsX Γ xcs" and  "x ∉ fst ` set xcs" 
  shows "wsX ((x, b, c1) #⇩Γ Γ)  xcs" 
  using assms proof(induct Γ)
  case GNil
  then show ?case using atom_dom.simps wsX_iff by auto
next
  case (GCons xbc Γ)
  obtain x' and b' and c' where xbc: "xbc = (x',b',c')" using prod_cases3 by blast
  then have "atom ` fst ` set xcs ⊆ atom_dom (xbc #⇩Γ Γ) ∧ distinct (map fst xcs)"
    using GCons.prems(1) wsX_iff by blast then show ?case by (simp add: Un_commute subset_Un_eq wsX_if2) 
qed

lemma wsX_cons3:
  assumes  "wsX Γ xcs"  
  shows "wsX ((x, b, c1) #⇩Γ Γ)  xcs" 
  using assms proof(induct Γ)
  case GNil
  then show ?case using atom_dom.simps wsX_iff by auto
next
  case (GCons xbc Γ)
  obtain x' and b' and c' where xbc: "xbc = (x',b',c')" using prod_cases3 by blast
  then have "atom ` fst ` set xcs ⊆ atom_dom (xbc #⇩Γ Γ) ∧ distinct (map fst xcs)"
    using GCons.prems(1) wsX_iff by blast then show ?case by (simp add: Un_commute subset_Un_eq wsX_if2) 
qed

lemma wsX_fresh:
  assumes "wsX G xcs" and "atom x ♯ G" and "wfG Θ ℬ G "
  shows "x ∉ fst ` set xcs"
proof - 
  have "atom x ∉ atom_dom G" using assms 
    using fresh_def wfG_dom_supp by auto
  thus ?thesis using wsX_iff assms by blast
qed

lemma replace_in_g_dist:
  assumes "x' ≠ x" 
  shows "replace_in_g ((x, b,c) #⇩Γ G) x' c'' = ((x, b,c) #⇩Γ (replace_in_g G x' c''))" using replace_in_g.simps assms by presburger

lemma wfG_replace_inside_rig:
  fixes c''::c
  assumes ‹Θ; ℬ ⊢⇩w⇩f G[x'⟼c'']› ‹Θ; ℬ ⊢⇩w⇩f (x, b, c) #⇩Γ G ›
  shows "Θ; ℬ ⊢⇩w⇩f (x, b, c) #⇩Γ G[x'⟼c'']"
proof(rule wfG_consI)

  have "wfG Θ ℬ G " using wfG_cons assms by auto

  show *:"Θ; ℬ ⊢⇩w⇩f G[x'⟼c'']" using assms by auto
  show "atom x ♯ G[x'⟼c'']" using replace_in_g_fresh_single[OF *] assms wfG_elims assms by metis
  show **:"Θ; ℬ ⊢⇩w⇩f b " using wfG_elim2 assms by auto
  show "Θ; ℬ; (x, b, TRUE) #⇩Γ G[x'⟼c'']  ⊢⇩w⇩f c "
  proof(cases "atom x' ∉ atom_dom G")
    case True
    hence "G = G[x'⟼c'']" using replace_in_g_forget ‹wfG Θ ℬ G›  by auto
    thus ?thesis using assms wfG_wfC by auto
  next
    case False
    then obtain G1 G2 b' c' where **:"G=G1@(x',b',c')#⇩ΓG2"
      using split_G by fastforce
    hence ***: "(G[x'⟼c'']) = G1@(x',b',c'')#⇩ΓG2"
      using replace_in_g_inside ‹wfG Θ ℬ G ›  by metis
    hence "Θ; ℬ; (x, b, TRUE) #⇩Γ G1@(x',b',c')#⇩ΓG2  ⊢⇩w⇩f c" using * ** assms wfG_wfC by auto
    hence  "Θ; ℬ; (x, b, TRUE) #⇩Γ G1@(x',b',c'')#⇩ΓG2  ⊢⇩w⇩f c" using * *** wf_replace_inside assms
      by (metis "**" append_g.simps(2) wfG_elim2 wfG_suffix)
    thus ?thesis using ** * *** by auto
  qed
qed

lemma replace_in_g_valid_weakening:
  assumes "Θ; ℬ; Γ[x'⟼c''] ⊨ c'" and "x' ≠ x" and  "Θ; ℬ ⊢⇩w⇩f (x, b, c) #⇩Γ Γ[x'⟼c'']"
  shows "Θ; ℬ; ((x, b,c) #⇩Γ Γ)[x'⟼ c'']  ⊨ c'"
  apply(subst replace_in_g_dist,simp add: assms,rule valid_weakening)
  using assms by auto+

lemma replace_in_g_subtyped_cons:
  assumes "replace_in_g_subtyped Θ ℬ G xcs G'"  and "wfG Θ ℬ ((x,b,c)#⇩ΓG)"
  shows "x ∉ fst ` set xcs ⟹ replace_in_g_subtyped Θ ℬ ((x,b,c)#⇩ΓG) xcs ((x,b,c)#⇩ΓG')"
  using assms proof(induct  rule: replace_in_g_subtyped.induct)
  case (replace_in_g_subtyped_nilI G)
  then show ?case 
    by (simp add: replace_in_g_subtyped.replace_in_g_subtyped_nilI)
next
  case (replace_in_g_subtyped_consI b' c' G x' Θ ℬ c'' xcs' G')
  hence "Θ; ℬ ⊢⇩w⇩f G[x'⟼c'']" using valid.simps wfC_wf by auto

  show ?case proof(rule replace_in_g_subtyped.replace_in_g_subtyped_consI)
    show  " Some (b', c') = lookup ((x, b,c) #⇩Γ G) x'" using lookup.simps 
        fst_conv image_iff Γ_set_intros surj_pair replace_in_g_subtyped_consI by force
    show wbc: " Θ; ℬ; (x, b, c) #⇩Γ G  ⊢⇩w⇩f c'' "  using wf_weakening ‹ Θ; ℬ; G ⊢⇩w⇩f c''› ‹Θ; ℬ  ⊢⇩w⇩f (x, b, c) #⇩Γ G › by fastforce
    have  "x' ≠ x"  using replace_in_g_subtyped_consI by auto
    have wbc1: "Θ; ℬ ⊢⇩w⇩f (x, b, c) #⇩Γ G[x'⟼c'']" proof -
      have "(x, b, c) #⇩Γ G[x'⟼c''] = ((x, b, c) #⇩Γ G)[x'⟼c'']" using ‹x' ≠ x› using replace_in_g.simps by auto
      thus  ?thesis using wfG_replace_inside_rig ‹Θ; ℬ ⊢⇩w⇩f G[x'⟼c'']›  ‹Θ; ℬ  ⊢⇩w⇩f (x, b, c) #⇩Γ G › by fastforce   
    qed
    show  *: "Θ; ℬ; replace_in_g ((x, b,c) #⇩Γ G) x' c''  ⊨ c'" 
    proof - 
      have "Θ; ℬ; G[x'⟼c'']  ⊨ c'" using replace_in_g_subtyped_consI by auto
      thus ?thesis using replace_in_g_valid_weakening wbc1 ‹x'≠x› by auto     
    qed

    show  "replace_in_g_subtyped Θ ℬ (replace_in_g ((x, b,c) #⇩Γ G) x' c'') xcs' ((x, b,c) #⇩Γ G')"  
      using replace_in_g_subtyped_consI wbc1 by auto
    show  "x' ∉ fst ` set xcs'" 
      using replace_in_g_subtyped_consI by linarith
  qed
qed

lemma replace_in_g_split:
  fixes G::Γ 
  assumes "Γ = replace_in_g Γ' x c" and "Γ' =  G'@(x,b,c')#⇩ΓG" and "wfG Θ ℬ Γ'"
  shows "Γ =  G'@(x,b,c)#⇩ΓG" 
  using assms proof(induct G' arbitrary: G Γ Γ' rule: Γ_induct)
  case GNil
  then show ?case by simp
next
  case (GCons x1 b1 c1 Γ1)
  hence "x1 ≠ x"
    using wfG_cons_fresh2[of Θ ℬ x1 b1 c1 Γ1 x b ] 
    using GCons.prems(2) GCons.prems(3) append_g.simps(2) by auto
  moreover hence *: "Θ; ℬ  ⊢⇩w⇩f  (Γ1 @ (x, b, c') #⇩Γ G)" using GCons append_g.simps wfG_elims by metis
  moreover hence "replace_in_g (Γ1 @ (x, b, c') #⇩Γ G) x c = Γ1 @ (x, b, c) #⇩Γ G" using GCons replace_in_g_inside[OF *, of c] by auto

  ultimately  show ?case using replace_in_g.simps(2)[of x1 b1 c1 " Γ1 @ (x, b, c') #⇩Γ G" x c] GCons
    by (simp add: GCons.prems(1) GCons.prems(2)) 
qed

lemma replace_in_g_subtyped_split0:
  fixes G::Γ 
  assumes "replace_in_g_subtyped Θ ℬ Γ'[(x,c)] Γ" and "Γ' =  G'@(x,b,c')#⇩ΓG"  and "wfG Θ ℬ Γ'"
  shows "Γ =  G'@(x,b,c)#⇩ΓG" 
proof - 
  have "Γ = replace_in_g Γ' x c" using assms replace_in_g_subtyped.simps
    by (metis Pair_inject list.distinct(1) list.inject)
  thus ?thesis using assms replace_in_g_split by blast
qed

lemma replace_in_g_subtyped_split:
  assumes "Some (b, c') = lookup G x" and "Θ; ℬ; replace_in_g G x c  ⊨ c'" and "wfG Θ ℬ G "
  shows "∃ Γ Γ'. G = Γ'@(x,b,c')#⇩ΓΓ ∧ Θ; ℬ; Γ'@(x,b,c)#⇩ΓΓ ⊨ c'"
proof -
  obtain Γ and Γ' where "G = Γ'@(x,b,c')#⇩ΓΓ" using assms lookup_split by blast
  moreover hence  "replace_in_g G x c =  Γ'@(x,b,c)#⇩ΓΓ" using replace_in_g_split assms by blast
  ultimately show ?thesis by (metis assms(2))
qed

section ‹Validity and Subtyping›

lemma wfC_replace_in_g:
  fixes c::c and c0::c
  assumes "Θ; ℬ; Γ'@(x,b,c0')#⇩ΓΓ ⊢⇩w⇩f c" and "Θ; ℬ; (x,b,TRUE)#⇩ΓΓ ⊢⇩w⇩f c0"
  shows "Θ; ℬ; Γ' @ (x, b, c0) #⇩Γ Γ ⊢⇩w⇩f c"
  using wf_replace_inside1(2) assms by auto 


lemma ctx_subtype_valid:
  assumes "Θ; ℬ; Γ'@(x,b,c0')#⇩ΓΓ ⊨ c" and 
    "Θ; ℬ; Γ'@(x,b,c0)#⇩ΓΓ ⊨ c0'"
  shows "Θ; ℬ; Γ'@(x,b,c0)#⇩ΓΓ ⊨ c"
proof(rule validI)
  show "Θ; ℬ; Γ' @ (x, b, c0) #⇩Γ Γ ⊢⇩w⇩f c" proof - 
    have  "Θ; ℬ; Γ'@(x,b,c0')#⇩ΓΓ ⊢⇩w⇩f c" using valid.simps assms by auto
    moreover have "Θ; ℬ; (x,b,TRUE)#⇩ΓΓ ⊢⇩w⇩f c0" proof -
      have "wfG Θ ℬ (Γ'@(x,b,c0)#⇩ΓΓ)" using assms valid.simps wfC_wf by auto
      hence "wfG Θ ℬ ((x,b,c0)#⇩ΓΓ)" using wfG_suffix by auto
      thus ?thesis using wfG_wfC by auto
    qed
    ultimately show ?thesis using assms wfC_replace_in_g by auto
  qed

  show "∀i. wfI Θ (Γ' @ (x, b, c0) #⇩Γ Γ) i ∧ is_satis_g i (Γ' @ (x, b, c0) #⇩Γ Γ) ⟶ is_satis i c" proof(rule,rule)
    fix i
    assume * : "wfI Θ (Γ' @ (x, b, c0) #⇩Γ Γ) i ∧ is_satis_g i (Γ' @ (x, b, c0) #⇩Γ Γ) "

    hence "is_satis_g i (Γ'@(x, b, c0) #⇩Γ Γ) ∧ wfI Θ (Γ'@(x, b, c0) #⇩Γ Γ) i" using is_satis_g_append wfI_suffix by metis
    moreover hence "is_satis i c0'" using valid.simps assms by presburger

    moreover have "is_satis_g i Γ'"  using is_satis_g_append * by simp
    ultimately have "is_satis_g i (Γ' @ (x, b, c0') #⇩Γ Γ) " using is_satis_g_append by simp
    moreover have "wfI Θ (Γ' @ (x, b, c0') #⇩Γ Γ) i" using wfI_def wfI_suffix * wfI_def wfI_replace_inside by metis
    ultimately show  "is_satis i c" using assms valid.simps by metis
  qed
qed

lemma ctx_subtype_subtype:
  fixes Γ::Γ
  shows "Θ; ℬ; G ⊢ t1 ≲ t2 ⟹ G = Γ'@(x,b0,c0')#⇩ΓΓ ⟹ Θ; ℬ; Γ'@(x,b0,c0)#⇩ΓΓ ⊨ c0' ⟹ Θ; ℬ; Γ'@(x,b0,c0)#⇩ΓΓ ⊢ t1 ≲ t2"
proof(nominal_induct avoiding: c0 rule: subtype.strong_induct)

  case (subtype_baseI x' Θ ℬ Γ'' z c z' c' b)
  let ?Γc0 = "Γ'@(x,b0,c0)#⇩ΓΓ" 
  have wb1:  "wfG Θ ℬ ?Γc0" using valid.simps wfC_wf   subtype_baseI by metis
  show ?case proof
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ   ⊢⇩w⇩f ⦃ z : b  | c ⦄ › using  wfT_replace_inside2[OF _ wb1] subtype_baseI by metis
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ   ⊢⇩w⇩f ⦃ z' : b  | c' ⦄ › using  wfT_replace_inside2[OF _ wb1] subtype_baseI by metis
    have "atom x' ♯ Γ' @ (x, b0, c0) #⇩Γ Γ" using fresh_prodN subtype_baseI fresh_replace_inside wb1 subtype_wf wfX_wfY by metis
    thus  ‹atom x' ♯ (Θ, ℬ, Γ' @ (x, b0, c0) #⇩Γ Γ,  z,  c , z' , c' )›  using subtype_baseI fresh_prodN by metis
    have "Θ; ℬ; ((x', b, c[z::=V_var x']⇩v) #⇩Γ Γ') @ (x, b0, c0) #⇩Γ Γ  ⊨ c'[z'::=V_var x']⇩v " proof(rule ctx_subtype_valid)
      show 1: ‹Θ; ℬ; ((x', b, c[z::=V_var x']⇩v) #⇩Γ Γ') @ (x, b0, c0') #⇩Γ Γ  ⊨ c'[z'::=V_var x']⇩v › 
        using  subtype_baseI append_g.simps subst_defs by metis
      have *:"Θ; ℬ ⊢⇩w⇩f ((x', b, c[z::=V_var x']⇩v) #⇩Γ Γ') @ (x, b0, c0) #⇩Γ Γ " proof(rule wfG_replace_inside2)
        show "Θ; ℬ ⊢⇩w⇩f ((x', b, c[z::=V_var x']⇩v) #⇩Γ Γ') @ (x, b0, c0') #⇩Γ Γ" 
          using * valid_wf_all wfC_wf 1 append_g.simps by metis
        show "Θ; ℬ ⊢⇩w⇩f (x, b0, c0) #⇩Γ Γ" using wfG_suffix wb1 by auto
      qed
      moreover have "toSet (Γ' @ (x, b0, c0) #⇩Γ Γ) ⊆ toSet (((x', b, c[z::=V_var x']⇩v) #⇩Γ Γ') @ (x, b0, c0) #⇩Γ Γ)" using toSet.simps append_g.simps by auto
      ultimately show  ‹Θ; ℬ; ((x', b, c[z::=V_var x']⇩v) #⇩Γ Γ') @ (x, b0, c0) #⇩Γ Γ  ⊨ c0' › using   valid_weakening subtype_baseI * by blast
    qed
    thus  ‹Θ; ℬ;  (x', b, c[z::=V_var x']⇩v) #⇩Γ Γ'  @ (x, b0, c0) #⇩Γ Γ  ⊨ c'[z'::=V_var x']⇩v › using append_g.simps subst_defs by simp     
  qed
qed

lemma ctx_subtype_subtype_rig:
  assumes   "replace_in_g_subtyped Θ  ℬ Γ' [(x,c0)] Γ" and  "Θ; ℬ; Γ' ⊢ t1 ≲ t2"  
  shows "Θ; ℬ; Γ ⊢ t1 ≲ t2"
proof -
  have wf: "wfG Θ ℬ Γ'" using subtype_g_wf assms by auto
  obtain b and c0' where  "Some (b, c0') = lookup Γ' x ∧ (Θ; ℬ; replace_in_g Γ' x c0  ⊨ c0')" using 
      replace_in_g_subtyped.simps[of  Θ ℬ Γ' "[(x, c0)]" Γ] assms(1) 

    by (metis fst_conv list.inject list.set_intros(1) list.simps(15) not_Cons_self2 old.prod.exhaust prod.inject set_ConsD surj_pair)
  moreover then obtain G and G' where *: "Γ' = G'@(x,b,c0')#⇩ΓG ∧ Θ; ℬ; G'@(x,b,c0)#⇩ΓG ⊨ c0'" 
    using replace_in_g_subtyped_split[of b  c0' Γ' x Θ ℬ c0] wf by metis

  ultimately show ?thesis using ctx_subtype_subtype 
      assms(1) assms(2) replace_in_g_subtyped_split0 subtype_g_wf  
    by (metis (no_types, lifting) local.wf replace_in_g_split)
qed

text ‹ We now prove versions of the @{text "ctx_subtype"} lemmas above using @{text "replace_in_g"}. First we do case where
the replace is just for a single variable (indicated by suffix rig) and then the general case for
multiple replacements (indicated by suffix rigs)›

lemma ctx_subtype_subtype_rigs:
  assumes "replace_in_g_subtyped Θ ℬ Γ' xcs Γ" and  "Θ; ℬ; Γ' ⊢ t1 ≲ t2"  
  shows "Θ; ℬ; Γ ⊢ t1 ≲ t2"
  using assms proof(induct xcs arbitrary: Γ Γ'  )
  case Nil  
  moreover have "Γ' = Γ" using replace_in_g_subtyped_nilI 
    using calculation(1) by blast
  ultimately show ?case by auto
next
  case (Cons a xcs)

  then obtain x and c where "a=(x,c)" by fastforce
  then obtain b and c' where bc: "Some (b, c') = lookup Γ' x ∧
         replace_in_g_subtyped Θ  ℬ (replace_in_g Γ' x c) xcs Γ ∧   Θ; ℬ; Γ'  ⊢⇩w⇩f c  ∧
         x ∉ fst ` set xcs ∧  Θ; ℬ; (replace_in_g Γ' x c)  ⊨ c' " using replace_in_g_subtyped_elims(3)[of Θ ℬ Γ' x c xcs Γ] Cons
    by (metis valid.simps)

  hence *: "replace_in_g_subtyped Θ ℬ Γ' [(x,c)] (replace_in_g Γ' x c)" using replace_in_g_subtyped_consI 
    by (meson image_iff list.distinct(1) list.set_cases replace_in_g_subtyped_nilI)

  hence "Θ; ℬ; (replace_in_g Γ' x c) ⊢  t1 ≲ t2"
    using  ctx_subtype_subtype_rig * assms Cons.prems(2) by auto

  moreover have "replace_in_g_subtyped Θ ℬ (replace_in_g Γ' x c) xcs Γ" using Cons
    using bc by blast

  ultimately show ?case using Cons by blast
qed

lemma replace_in_g_inside_valid:
  assumes "replace_in_g_subtyped Θ ℬ Γ' [(x,c0)] Γ" and "wfG Θ ℬ Γ'"
  shows "∃b c0' G G'. Γ' = G' @ (x,b,c0')#⇩ΓG ∧  Γ = G' @ (x,b,c0)#⇩ΓG ∧ Θ; ℬ; G'@ (x,b,c0)#⇩ΓG  ⊨ c0'"
proof - 
  obtain b and c0' where  bc: "Some (b, c0') = lookup Γ' x ∧ Θ; ℬ; replace_in_g Γ' x c0  ⊨ c0'" using 
      replace_in_g_subtyped.simps[of  Θ ℬ Γ' "[(x, c0)]" Γ] assms(1) 
    by (metis fst_conv list.inject list.set_intros(1) list.simps(15) not_Cons_self2 old.prod.exhaust prod.inject set_ConsD surj_pair)
  then obtain G and G' where *: "Γ' = G'@(x,b,c0')#⇩ΓG ∧ Θ; ℬ; G'@(x,b,c0)#⇩ΓG ⊨ c0'" using replace_in_g_subtyped_split[of b c0' Γ' x Θ ℬ c0] assms
    by metis
  thus ?thesis using replace_in_g_inside bc
    using assms(1) assms(2) by blast
qed

lemma replace_in_g_valid:
  assumes "Θ; ℬ  ⊢ G ⟨ xcs ⟩ ↝ G'" and  "Θ; ℬ; G  ⊨ c "
  shows  ‹Θ; ℬ; G'  ⊨ c ›
  using assms proof(induct rule: replace_in_g_subtyped.inducts)
  case (replace_in_g_subtyped_nilI Θ ℬ G)
  then show ?case by auto
next
  case (replace_in_g_subtyped_consI b c1 G x Θ ℬ c2 xcs G')
  hence "Θ; ℬ; G[x⟼c2]  ⊨ c" 
    by (metis ctx_subtype_valid replace_in_g_split replace_in_g_subtyped_split valid_g_wf)
  then show ?case using replace_in_g_subtyped_consI by auto
qed

section ‹Literals›

section ‹Values›

lemma lookup_inside_unique_b[simp]:
  assumes "Θ ; B ⊢⇩w⇩f (Γ'@(x,b0,c0)#⇩ΓΓ)" and "Θ ; B ⊢⇩w⇩f (Γ'@(x,b0,c0')#⇩ΓΓ)"
    and  "Some (b, c) = lookup (Γ' @ (x, b0, c0') #⇩Γ Γ) y" and  "Some (b0,c0) = lookup (Γ'@((x,b0,c0))#⇩ΓΓ) x" and "x=y"
  shows "b = b0"
  by (metis assms(2) assms(3) assms(5) lookup_inside_wf old.prod.exhaust option.inject prod.inject)

lemma ctx_subtype_v_aux:
  fixes v::v
  assumes  "Θ; ℬ; Γ'@((x,b0,c0')#⇩ΓΓ) ⊢ v ⇒ t1" and   "Θ; ℬ; Γ'@(x,b0,c0)#⇩ΓΓ ⊨ c0'" 
  shows "Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ) ⊢ v ⇒ t1"
  using assms proof(nominal_induct "Γ'@((x,b0,c0')#⇩ΓΓ)" v t1 avoiding: c0    rule: infer_v.strong_induct)
  case (infer_v_varI Θ ℬ b c xa z)
  have  wf:‹ Θ; ℬ  ⊢⇩w⇩f Γ' @ (x, b0, c0) #⇩Γ Γ › using wfG_inside_valid2 infer_v_varI by metis
  have  xf1:‹atom z ♯ xa› using  infer_v_varI by metis
  have  xf2: ‹atom z ♯ (Θ, ℬ, Γ' @ (x, b0, c0) #⇩Γ Γ)› apply( fresh_mth add:  infer_v_varI )
    using fresh_def infer_v_varI wfG_supp fresh_append_g fresh_GCons fresh_prodN by metis+
  show ?case proof (cases "x=xa")
    case True
    moreover have "b = b0" using infer_v_varI True by simp
    moreover hence  ‹Some (b, c0) = lookup (Γ' @ (x, b0, c0) #⇩Γ Γ) xa› using   lookup_inside_wf[OF wf] infer_v_varI True by auto
    ultimately show ?thesis using  wf xf1 xf2 Typing.infer_v_varI by metis
  next
    case False
    moreover hence  ‹Some (b, c) = lookup (Γ' @ (x, b0, c0) #⇩Γ Γ) xa› using   lookup_inside2 infer_v_varI by metis
    ultimately show ?thesis using wf xf1 xf2 Typing.infer_v_varI by simp
  qed   
next
  case (infer_v_litI Θ ℬ l τ)
  thus ?case using Typing.infer_v_litI wfG_inside_valid2 by simp
next
  case (infer_v_pairI z v1 v2 Θ ℬ t1' t2' c0)
  show  ?case proof
    show "atom z ♯ (v1, v2)" using infer_v_pairI fresh_Pair by simp
    show "atom z ♯ (Θ, ℬ, Γ' @ (x, b0, c0) #⇩Γ Γ)"  apply( fresh_mth add:  infer_v_pairI )
      using fresh_def infer_v_pairI wfG_supp fresh_append_g fresh_GCons fresh_prodN by metis+
    show "Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ ⊢ v1 ⇒ t1'" using infer_v_pairI  by simp
    show "Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ ⊢ v2 ⇒ t2'" using infer_v_pairI  by simp
  qed   
next
  case (infer_v_consI s dclist Θ dc tc ℬ v tv z)
  show ?case proof
    show ‹AF_typedef s dclist ∈ set Θ› using infer_v_consI by auto
    show ‹(dc, tc) ∈ set dclist› using infer_v_consI by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ ⊢ v ⇒ tv› using infer_v_consI by auto
    show ‹Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ tv ≲ tc› using infer_v_consI ctx_subtype_subtype by auto
    show ‹atom z ♯ v› using infer_v_consI by auto
    show ‹atom z ♯ (Θ, ℬ, Γ' @ (x, b0, c0) #⇩Γ Γ)› apply( fresh_mth add:  infer_v_consI )
      using fresh_def infer_v_consI wfG_supp fresh_append_g fresh_GCons fresh_prodN by metis+
  qed
next
  case (infer_v_conspI s bv dclist Θ dc tc ℬ v tv b z)
  show ?case proof
    show ‹AF_typedef_poly s bv dclist ∈ set Θ› using infer_v_conspI by auto
    show ‹(dc, tc) ∈ set dclist›  using infer_v_conspI by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ ⊢ v ⇒ tv›  using infer_v_conspI by auto
    show ‹Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ tv ≲ tc[bv::=b]⇩τ⇩b›  using infer_v_conspI ctx_subtype_subtype by auto
    show ‹atom z ♯ (Θ, ℬ, Γ' @ (x, b0, c0) #⇩Γ Γ, v, b)›  apply( fresh_mth add:  infer_v_conspI )
      using fresh_def infer_v_conspI wfG_supp fresh_append_g fresh_GCons fresh_prodN by metis+
    show ‹atom bv ♯ (Θ, ℬ, Γ' @ (x, b0, c0) #⇩Γ Γ, v, b)› apply( fresh_mth add:  infer_v_conspI )
      using fresh_def infer_v_conspI wfG_supp fresh_append_g fresh_GCons fresh_prodN by metis+
    show ‹ Θ; ℬ  ⊢⇩w⇩f b ›  using infer_v_conspI by auto
  qed
qed

lemma ctx_subtype_v:
  fixes v::v
  assumes  "Θ; ℬ; Γ'@((x,b0,c0')#⇩ΓΓ) ⊢ v ⇒ t1" and   "Θ; ℬ; Γ'@(x,b0,c0)#⇩ΓΓ ⊨ c0'" 
  shows "∃t2.  Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ) ⊢ v ⇒ t2 ∧  Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ) ⊢ t2 ≲ t1"
proof -

  have "Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ) ⊢ v ⇒ t1 " using ctx_subtype_v_aux assms by auto
  moreover hence "Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ) ⊢ t1 ≲ t1" using subtype_reflI2 infer_v_wf by simp
  ultimately show ?thesis by auto
qed

lemma ctx_subtype_v_eq:
  fixes v::v
  assumes
    "Θ; ℬ; Γ'@((x,b0,c0')#⇩ΓΓ) ⊢ v ⇒ t1" and 
    " Θ; ℬ; Γ'@(x,b0,c0)#⇩ΓΓ ⊨ c0'" 
  shows "Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ) ⊢ v ⇒ t1"
proof - 
  obtain t1' where "Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ) ⊢ v ⇒ t1'" using ctx_subtype_v assms by metis
  moreover have "replace_in_g (Γ'@((x,b0,c0')#⇩ΓΓ)) x c0 =  Γ'@((x,b0,c0)#⇩ΓΓ)" using replace_in_g_inside infer_v_wf assms by metis
  ultimately show ?thesis using infer_v_uniqueness_rig assms by metis
qed

lemma ctx_subtype_check_v_eq:
  assumes  "Θ; ℬ; Γ'@((x,b0,c0')#⇩ΓΓ) ⊢ v ⇐ t1" and " Θ; ℬ; Γ'@(x,b0,c0)#⇩ΓΓ ⊨ c0'"
  shows "Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ) ⊢ v ⇐ t1"
proof - 
  obtain t2 where t2: "Θ; ℬ; Γ'@((x,b0,c0')#⇩ΓΓ) ⊢ v ⇒ t2 ∧   Θ; ℬ; Γ'@((x,b0,c0')#⇩ΓΓ) ⊢ t2 ≲ t1" 
    using check_v_elims assms by blast
  hence t3: "Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ)  ⊢ v ⇒ t2"
    using assms ctx_subtype_v_eq by blast

  have "Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ)  ⊢ v ⇒ t2" using t3 by auto
  moreover have " Θ; ℬ; Γ'@((x,b0,c0)#⇩ΓΓ)  ⊢ t2 ≲ t1" proof -

    have " Θ; ℬ; Γ'@((x,b0,c0')#⇩ΓΓ) ⊢ t2 ≲ t1" using t2 by auto
    thus  ?thesis using subtype_trans
      using assms(2) ctx_subtype_subtype by blast
  qed
  ultimately show ?thesis using check_v.intros by presburger 
qed

text ‹ Basically the same as @{text "ctx_subtype_v_eq"} but in a different form›
lemma ctx_subtype_v_rig_eq:
  fixes v::v
  assumes "replace_in_g_subtyped  Θ ℬ Γ' [(x,c0)] Γ" and  
    "Θ; ℬ; Γ'  ⊢ v ⇒ t1" 
  shows "Θ; ℬ; Γ ⊢ v ⇒ t1"
proof - 
  obtain b and c0' and G and G' where "Γ' = G' @ (x,b,c0')#⇩ΓG ∧  Γ = G' @ (x,b,c0)#⇩ΓG ∧  Θ; ℬ; G'@ (x,b,c0)#⇩ΓG  ⊨ c0'"
    using assms replace_in_g_inside_valid  infer_v_wf by metis
  thus ?thesis using ctx_subtype_v_eq[of Θ ℬ G' x b c0' G v t1 c0] assms by simp
qed

lemma ctx_subtype_v_rigs_eq:
  fixes v::v
  assumes "replace_in_g_subtyped Θ ℬ Γ' xcs Γ" and  
    "Θ; ℬ; Γ'  ⊢ v ⇒ t1" 
  shows "Θ; ℬ; Γ ⊢ v ⇒ t1"
  using assms proof(induct xcs arbitrary: Γ Γ' t1 )
  case Nil
  then show ?case by auto
next
  case (Cons a xcs)
  then obtain x and c where "a=(x,c)" by fastforce

  then obtain b and c' where bc: "Some (b, c') = lookup Γ' x ∧
         replace_in_g_subtyped  Θ ℬ (replace_in_g Γ' x c) xcs Γ ∧  Θ; ℬ; Γ'  ⊢⇩w⇩f c ∧
         x ∉ fst ` set xcs ∧   Θ; ℬ; (replace_in_g Γ' x c)  ⊨ c' "   
    using replace_in_g_subtyped_elims(3)[of  Θ ℬ Γ' x c xcs Γ] Cons  by (metis valid.simps)

  hence *: "replace_in_g_subtyped  Θ ℬ Γ' [(x,c)] (replace_in_g Γ' x c)" using replace_in_g_subtyped_consI 
    by (meson image_iff list.distinct(1) list.set_cases replace_in_g_subtyped_nilI)
  hence   t2: "Θ; ℬ; (replace_in_g Γ' x c) ⊢ v ⇒ t1 " using ctx_subtype_v_rig_eq[OF * Cons(3)] by blast
  moreover have **: "replace_in_g_subtyped  Θ ℬ (replace_in_g Γ' x c) xcs Γ" using bc by auto
  ultimately have  t2': "Θ; ℬ; Γ ⊢ v ⇒ t1" using Cons by blast
  thus ?case by blast
qed

lemma ctx_subtype_check_v_rigs_eq:
  assumes "replace_in_g_subtyped Θ ℬ Γ' xcs Γ" and  
    "Θ; ℬ; Γ'  ⊢ v ⇐ t1" 
  shows "Θ; ℬ; Γ ⊢ v ⇐ t1"
proof - 
  obtain t2 where  "Θ; ℬ; Γ'  ⊢ v ⇒ t2 ∧  Θ; ℬ; Γ' ⊢ t2 ≲ t1" using check_v_elims assms by fast
  hence "Θ; ℬ; Γ  ⊢ v ⇒ t2 ∧  Θ; ℬ; Γ ⊢ t2 ≲ t1" using ctx_subtype_v_rigs_eq ctx_subtype_subtype_rigs 
    using assms(1) by blast
  thus ?thesis 
    using check_v_subtypeI by blast
qed

section ‹Expressions›

lemma valid_wfC:
  fixes c0::c
  assumes  "Θ; ℬ; Γ'@(x,b0,c0)#⇩ΓΓ ⊨ c0'" 
  shows "Θ; ℬ; (x, b0, TRUE) #⇩Γ Γ  ⊢⇩w⇩f c0"
  using  wfG_elim2 valid.simps wfG_suffix 
  using assms valid_g_wf by metis

lemma ctx_subtype_e_eq:
  fixes G::Γ
  assumes
    "Θ ; Φ ; ℬ ; G ; Δ ⊢ e ⇒ t1" and "G =  Γ'@((x,b0,c0')#⇩ΓΓ)"
    "Θ; ℬ; Γ'@(x,b0,c0)#⇩ΓΓ ⊨ c0'" 
  shows "Θ ; Φ ; ℬ ; Γ'@((x,b0,c0)#⇩ΓΓ) ; Δ ⊢ e ⇒ t1"
  using assms proof(nominal_induct t1 avoiding: c0 rule: infer_e.strong_induct)
  case (infer_e_valI Θ ℬ Γ'' Δ Φ v τ)
  show ?case proof
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_valI by auto
    show ‹ Θ  ⊢⇩w⇩f Φ › using infer_e_valI by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v ⇒ τ› using infer_e_valI ctx_subtype_v_eq by auto
  qed
next
  case (infer_e_plusI Θ ℬ Γ'' Δ Φ v1 z1 c1 v2 z2 c2 z3)
  show ?case proof 
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_plusI by auto
    show ‹ Θ  ⊢⇩w⇩f Φ ›  using infer_e_plusI by auto
    show *:‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v1 ⇒ ⦃ z1 : B_int  | c1 ⦄› using infer_e_plusI ctx_subtype_v_eq by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v2 ⇒ ⦃ z2 : B_int  | c2 ⦄› using infer_e_plusI ctx_subtype_v_eq by auto
    show ‹atom z3 ♯ AE_op Plus v1 v2› using infer_e_plusI by auto
    show   ‹atom z3 ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using * infer_e_plusI fresh_replace_inside  infer_v_wf  by metis
  qed
next
  case (infer_e_leqI Θ ℬ Γ'' Δ Φ v1 z1 c1 v2 z2 c2 z3)
  show ?case proof 
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_leqI by auto
    show ‹ Θ  ⊢⇩w⇩f Φ ›  using infer_e_leqI by auto
    show *:‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v1 ⇒ ⦃ z1 : B_int  | c1 ⦄› using infer_e_leqI ctx_subtype_v_eq by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v2 ⇒ ⦃ z2 : B_int  | c2 ⦄› using infer_e_leqI ctx_subtype_v_eq by auto
    show ‹atom z3 ♯ AE_op LEq v1 v2› using infer_e_leqI by auto
    show   ‹atom z3 ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using * infer_e_leqI fresh_replace_inside  infer_v_wf  by metis
  qed
next
  case (infer_e_eqI Θ ℬ Γ'' Δ Φ v1 z1 bb c1 v2 z2 c2 z3)
  show ?case proof 
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_eqI by auto
    show ‹ Θ  ⊢⇩w⇩f Φ ›  using infer_e_eqI by auto
    show *:‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v1 ⇒ ⦃ z1 : bb  | c1 ⦄› using infer_e_eqI ctx_subtype_v_eq by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v2 ⇒ ⦃ z2 : bb  | c2 ⦄› using infer_e_eqI ctx_subtype_v_eq by auto
    show ‹atom z3 ♯ AE_op Eq v1 v2› using infer_e_eqI by auto
    show   ‹atom z3 ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using * infer_e_eqI fresh_replace_inside  infer_v_wf  by metis
    show "bb ∈ {B_bool, B_int, B_unit}" using infer_e_eqI by auto
  qed
next
  case (infer_e_appI Θ ℬ Γ'' Δ Φ f x' b c τ' s' v τ)
  show ?case proof
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_appI by auto
    show ‹ Θ  ⊢⇩w⇩f Φ › using  infer_e_appI by auto
    show ‹Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x' b c τ' s'))) = lookup_fun Φ f›  using infer_e_appI by auto
    show ‹Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v ⇐ ⦃ x' : b  | c ⦄› using infer_e_appI ctx_subtype_check_v_eq by auto
    thus ‹atom x' ♯ (Θ, Φ, ℬ, Γ' @ (x, b0, c0) #⇩Γ Γ, Δ, v, τ)› 
      using infer_e_appI fresh_replace_inside[of Θ ℬ Γ' x b0 c0' Γ c0 x']  infer_v_wf by auto
    show ‹τ'[x'::=v]⇩v = τ› using infer_e_appI by auto
  qed
next
  case (infer_e_appPI Θ ℬ Γ1 Δ Φ b' f bv x1 b c τ' s' v τ)
  show ?case proof
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_appPI by auto
    show ‹ Θ  ⊢⇩w⇩f Φ › using infer_e_appPI by auto
    show ‹ Θ; ℬ  ⊢⇩w⇩f b' › using infer_e_appPI by auto
    show ‹Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x1 b c τ' s'))) = lookup_fun Φ f› using infer_e_appPI by auto
    show ‹Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v ⇐ ⦃ x1 : b[bv::=b']⇩b  | c[bv::=b']⇩b ⦄› using infer_e_appPI  ctx_subtype_check_v_eq subst_defs by auto
    thus  ‹atom x1 ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using  fresh_replace_inside[of Θ ℬ Γ' x b0 c0' Γ  c0 x1 ] infer_v_wf infer_e_appPI by auto
    show ‹τ'[bv::=b']⇩b[x1::=v]⇩v = τ› using infer_e_appPI by auto
    have "atom bv ♯ Γ' @ (x, b0, c0') #⇩Γ Γ" using infer_e_appPI by metis
    hence "atom bv ♯  Γ' @ (x, b0, c0) #⇩Γ Γ" 
      unfolding fresh_append_g fresh_GCons fresh_prod3 using  ‹atom bv ♯ c0 › fresh_append_g by metis
    thus  ‹atom bv ♯  (Θ, Φ, ℬ, Γ' @ (x, b0, c0) #⇩Γ Γ, Δ, b', v, τ)› using infer_e_appPI by auto
  qed
next
  case (infer_e_fstI Θ ℬ Γ'' Δ Φ v z' b1 b2 c z)
  show ?case proof 
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_fstI by auto
    show ‹ Θ ⊢⇩w⇩f Φ › using infer_e_fstI by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v ⇒ ⦃ z' : B_pair b1 b2  | c ⦄› using infer_e_fstI ctx_subtype_v_eq by auto
    thus ‹atom z ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using infer_e_fstI fresh_replace_inside[of Θ ℬ Γ' x b0 c0' Γ c0 z]  infer_v_wf by auto
    show ‹atom z ♯ AE_fst v› using infer_e_fstI by auto
  qed
next
  case (infer_e_sndI Θ ℬ Γ'' Δ Φ v z' b1 b2 c z)
  show ?case proof 
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_sndI by auto
    show ‹ Θ ⊢⇩w⇩f Φ › using infer_e_sndI by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v ⇒ ⦃ z' : B_pair b1 b2  | c ⦄› using infer_e_sndI ctx_subtype_v_eq by auto
    thus ‹atom z ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using infer_e_sndI fresh_replace_inside[of Θ ℬ Γ' x b0 c0' Γ c0 z]  infer_v_wf by auto
    show ‹atom z ♯ AE_snd v› using infer_e_sndI by auto
  qed
next
  case (infer_e_lenI Θ ℬ Γ'' Δ Φ v z' c z)
  show ?case proof 
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_lenI by auto
    show ‹ Θ ⊢⇩w⇩f Φ › using infer_e_lenI by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v ⇒ ⦃ z' : B_bitvec  | c ⦄› using infer_e_lenI ctx_subtype_v_eq by auto
    thus ‹atom z ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using infer_e_lenI fresh_replace_inside[of Θ ℬ Γ' x b0 c0' Γ c0 z]  infer_v_wf by auto
    show ‹atom z ♯ AE_len v› using infer_e_lenI by auto
  qed
next
  case (infer_e_mvarI Θ ℬ Γ'' Φ Δ u τ)
  show ?case proof 
    show "Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢⇩w⇩f Δ"   using wf_replace_inside2(6) valid_wfC infer_e_mvarI by auto
    thus "Θ; ℬ ⊢⇩w⇩f Γ' @ (x, b0, c0) #⇩Γ Γ" using infer_e_mvarI fresh_replace_inside  wfD_wf   by blast 
    show "Θ ⊢⇩w⇩f Φ "  using infer_e_mvarI by auto
    show "(u, τ) ∈ setD Δ" using infer_e_mvarI by auto
  qed
next
  case (infer_e_concatI Θ  ℬ Γ'' Δ Φ v1 z1 c1 v2 z2 c2 z3)
  show ?case proof 
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_concatI by auto
    thus  ‹atom z3 ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using infer_e_concatI fresh_replace_inside[of Θ ℬ Γ' x b0 c0' Γ c0 z3]  infer_v_wf wfX_wfY by metis
    show ‹ Θ ⊢⇩w⇩f Φ › using infer_e_concatI by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v1 ⇒ ⦃ z1 : B_bitvec  | c1 ⦄› using infer_e_concatI ctx_subtype_v_eq by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ  ⊢ v2 ⇒ ⦃ z2 : B_bitvec  | c2 ⦄› using infer_e_concatI ctx_subtype_v_eq by auto
    show ‹atom z3 ♯ AE_concat v1 v2› using infer_e_concatI by auto  
  qed
next
  case (infer_e_splitI Θ ℬ Γ'' Δ Φ v1 z1 c1 v2 z2 z3)
  show ?case proof
    show *:‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ ⊢⇩w⇩f Δ › using wf_replace_inside2(6) valid_wfC infer_e_splitI by auto  
    show ‹ Θ  ⊢⇩w⇩f Φ › using infer_e_splitI by auto
    show ‹ Θ; ℬ; Γ' @ (x, b0, c0) #⇩Γ Γ ⊢ v1 ⇒ ⦃ z1 : B_bitvec  | c1 ⦄› using infer_e_splitI  ctx_subtype_v_eq by auto
    show ‹Θ; ℬ; Γ' @
                 (x, b0, c0) #⇩Γ
                 Γ  ⊢ v2 ⇐ ⦃ z2 : B_int  | [ leq [ [ L_num 0 ]⇧v ]⇧c⇧e [ [ z2 ]⇧v ]⇧c⇧e ]⇧c⇧e  ==  [ [ L_true ]⇧v ]⇧c⇧e AND
                                 [ leq [ [ z2 ]⇧v ]⇧c⇧e [| [ v1 ]⇧c⇧e |]⇧c⇧e ]⇧c⇧e  ==  [ [ L_true ]⇧v ]⇧c⇧e   ⦄› 
      using infer_e_splitI  ctx_subtype_check_v_eq by auto

    show  ‹atom z1 ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using  fresh_replace_inside[of Θ ℬ Γ' x b0 c0' Γ c0 z1] infer_e_splitI  infer_v_wf wfX_wfY * by metis
    show  ‹atom z2 ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using  fresh_replace_inside[of Θ ℬ Γ' x b0 c0' Γ c0 ] infer_e_splitI  infer_v_wf wfX_wfY * by metis
    show  ‹atom z3 ♯ Γ' @ (x, b0, c0) #⇩Γ Γ› using  fresh_replace_inside[of Θ ℬ Γ' x b0 c0' Γ c0 ] infer_e_splitI  infer_v_wf wfX_wfY * by metis
    show ‹atom z1 ♯ AE_split v1 v2› using infer_e_splitI by auto
    show ‹atom z2 ♯ AE_split v1 v2› using infer_e_splitI by auto
    show ‹atom z3 ♯ AE_split v1 v2› using infer_e_splitI by auto
  qed
qed

lemma ctx_subtype_e_rig_eq:
  assumes "replace_in_g_subtyped Θ ℬ Γ' [(x,c0)] Γ" and  
    "Θ ; Φ ; ℬ ; Γ' ; Δ ⊢ e ⇒ t1" 
  shows "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ e ⇒ t1"
proof - 
  obtain b and c0' and G and G' where "Γ' = G' @ (x,b,c0')#⇩ΓG ∧  Γ = G' @ (x,b,c0)#⇩ΓG ∧  Θ; ℬ; G'@ (x,b,c0)#⇩ΓG  ⊨ c0'"
    using assms replace_in_g_inside_valid infer_e_wf by meson
  thus  ?thesis 
    using assms ctx_subtype_e_eq by presburger
qed

lemma ctx_subtype_e_rigs_eq:
  assumes "replace_in_g_subtyped Θ ℬ Γ' xcs Γ" and  
    "Θ ; Φ ; ℬ ; Γ'; Δ ⊢ e ⇒ t1" 
  shows "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ e ⇒ t1"
  using assms proof(induct xcs arbitrary: Γ Γ' t1 )
  case Nil
  moreover have "Γ' = Γ" using replace_in_g_subtyped_nilI 
    using calculation(1) by blast
  moreover have "Θ;ℬ;Γ ⊢ t1 ≲ t1" using subtype_reflI2 Nil infer_e_t_wf by blast
  ultimately show ?case by blast
next
  case (Cons a xcs)

  then obtain x and c where "a=(x,c)" by fastforce
  then obtain b and c' where bc: "Some (b, c') = lookup Γ' x ∧
         replace_in_g_subtyped Θ ℬ (replace_in_g Γ' x c) xcs Γ ∧ Θ; ℬ; Γ'  ⊢⇩w⇩f c ∧
         x ∉ fst ` set xcs ∧   Θ; ℬ; (replace_in_g Γ' x c)  ⊨ c' " using replace_in_g_subtyped_elims(3)[of  Θ ℬ Γ' x c xcs Γ] Cons
    by (metis valid.simps)

  hence *: "replace_in_g_subtyped Θ ℬ Γ' [(x,c)] (replace_in_g Γ' x c)" using replace_in_g_subtyped_consI 
    by (meson image_iff list.distinct(1) list.set_cases replace_in_g_subtyped_nilI)
  hence   t2: "Θ ; Φ ; ℬ ; (replace_in_g Γ' x c) ; Δ ⊢ e ⇒ t1 " using ctx_subtype_e_rig_eq[OF * Cons(3)] by blast
  moreover have **: "replace_in_g_subtyped  Θ ℬ (replace_in_g Γ' x c) xcs Γ" using bc by auto
  ultimately have  t2': "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ e ⇒ t1" using Cons by blast
  thus  ?case  by blast
qed

section ‹Statements›

lemma ctx_subtype_s_rigs:
  fixes c0::c and s::s and G'::Γ and xcs :: "(x*c) list" and css::branch_list
  shows
    "check_s Θ Φ ℬ G Δ  s  t1 ⟹ wsX G xcs  ⟹ replace_in_g_subtyped Θ ℬ G xcs G'  ⟹ check_s Θ Φ ℬ G' Δ  s  t1" and 
    "check_branch_s Θ Φ ℬ G Δ tid cons const v cs  t1 ⟹  wsX G xcs  ⟹ replace_in_g_subtyped  Θ ℬ G xcs G'  ⟹ check_branch_s Θ Φ ℬ G' Δ tid cons const v cs t1"
    "check_branch_list Θ Φ ℬ G Δ tid dclist v css  t1 ⟹  wsX G xcs  ⟹ replace_in_g_subtyped  Θ ℬ G xcs G'  ⟹ check_branch_list Θ Φ ℬ G' Δ tid dclist v css t1"
proof(induction   arbitrary:  xcs G' and xcs G' and xcs G' rule: check_s_check_branch_s_check_branch_list.inducts)
  case (check_valI Θ ℬ Γ Δ Φ v τ' τ)
  hence *:"Θ; ℬ; G'  ⊢ v ⇒ τ' ∧  Θ; ℬ; G'  ⊢ τ' ≲ τ" using ctx_subtype_v_rigs_eq ctx_subtype_subtype_rigs 
    by (meson check_v.simps)
  show ?case proof
    show ‹Θ; ℬ; G' ⊢⇩w⇩f Δ› using check_valI wfD_rig by auto
    show ‹Θ ⊢⇩w⇩f Φ › using check_valI by auto
    show ‹Θ; ℬ; G'  ⊢ v ⇒ τ'› using * by auto
    show ‹Θ; ℬ; G'  ⊢ τ' ≲ τ› using * by auto
  qed
next
  case (check_letI x Θ Φ ℬ Γ Δ e τ z' s b' c')

  show ?case proof
    have wfG: "Θ; ℬ ⊢⇩w⇩f Γ ∧ Θ; ℬ ⊢⇩w⇩f G'" using infer_e_wf check_letI replace_in_g_wfG   using infer_e_wf(2) by (auto simp add: freshers)
    hence "atom x ♯ G'" using check_letI replace_in_g_fresh replace_in_g_wfG  by auto
    thus  "atom x ♯ (Θ, Φ, ℬ, G', Δ, e, τ)" using check_letI by auto
    have "atom z' ♯ G'" apply(rule replace_in_g_fresh[OF check_letI(7)]) 
      using replace_in_g_wfG check_letI fresh_prodN infer_e_wf by metis+
    thus "atom z' ♯ (x, Θ, Φ, ℬ, G', Δ, e, τ, s)" using check_letI fresh_prodN by metis

    show "Θ ; Φ ; ℬ ; G' ; Δ  ⊢ e ⇒ ⦃ z' : b'  | c' ⦄" 
      using check_letI ctx_subtype_e_rigs_eq by blast 
    show "Θ ; Φ ; ℬ ; (x, b', c'[z'::=V_var x]⇩v) #⇩Γ G' ; Δ  ⊢ s ⇐ τ" 
    proof(rule  check_letI(5))
      have vld: "Θ;ℬ;((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ) ⊨  c'[z'::=V_var x]⇩c⇩v" proof -
        have "wfG Θ ℬ ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ)" using check_letI check_s_wf  by metis
        hence "wfC Θ ℬ ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ) (c'[z'::=V_var x]⇩c⇩v)" using wfC_refl subst_defs by auto
        thus ?thesis using  valid_reflI[of  Θ ℬ x b' "c'[z'::=V_var x]⇩v" Γ " c'[z'::=V_var x]⇩v"] subst_defs by auto
      qed
      have xf: "x ∉ fst ` set xcs" proof -
        have  "atom ` fst ` set xcs ⊆ atom_dom Γ" using check_letI wsX_iff by meson 
        moreover have "wfG Θ ℬ Γ" using infer_e_wf check_letI by metis
        ultimately show ?thesis using fresh_def  check_letI  wfG_dom_supp 
          using wsX_fresh by auto
      qed
      show "replace_in_g_subtyped Θ ℬ ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ) ((x, c'[z'::=V_var x]⇩v) # xcs) ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ G')" proof -

        have "Some (b', c'[z'::=V_var x]⇩v) =  lookup ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ) x" by auto

        moreover have "Θ; ℬ; replace_in_g ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ) x  (c'[z'::=V_var x]⇩v) ⊨  c'[z'::=V_var x]⇩v" proof -
          have "replace_in_g ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ) x  (c'[z'::=V_var x]⇩v) = ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ)" 
            using replace_in_g.simps by presburger
          thus ?thesis  using vld subst_defs by auto
        qed

        moreover have " replace_in_g_subtyped Θ ℬ (replace_in_g ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ) x (c'[z'::=V_var x]⇩v)) xcs ( ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ G'))" proof -
          have "wfG Θ ℬ ( ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ))"  using check_letI check_s_wf  by metis
          hence "replace_in_g_subtyped Θ ℬ ( ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ)) xcs ( ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ G'))" 
            using check_letI replace_in_g_subtyped_cons xf by meson
          moreover have "replace_in_g ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ) x (c'[z'::=V_var x]⇩v) = ( ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ))"
            using replace_in_g.simps by presburger
          ultimately show ?thesis by argo
        qed      
        moreover  have "Θ; ℬ; (x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ  ⊢⇩w⇩f  c'[z'::=V_var x]⇩v " using vld subst_defs by auto
        ultimately show ?thesis using  replace_in_g_subtyped_consI xf replace_in_g.simps(2) by metis
      qed

      show " wsX ((x, b', c'[z'::=V_var x]⇩v) #⇩Γ Γ) ((x, c'[z'::=V_var x]⇩v) # xcs)" 
        using check_letI xf subst_defs  by (simp add: wsX_cons)  
    qed
  qed

next
  case (check_branch_list_consI Θ Φ ℬ Γ Δ tid dclist v cs τ css)
  then show ?case using Typing.check_branch_list_consI by auto
next
  case (check_branch_list_finalI Θ Φ ℬ Γ Δ tid dclist v cs τ)
  then show ?case using Typing.check_branch_list_finalI by auto
next
  case (check_branch_s_branchI Θ ℬ Γ Δ τ const x Φ tid cons v s)

  have wfcons: "wfG Θ ℬ ((x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x))  AND c_of const x) #⇩Γ Γ)" using check_s_wf check_branch_s_branchI
    by meson
  hence wf: "wfG Θ ℬ Γ" using  wfG_cons by metis

  moreover have "atom x ♯ (const, G',v)"  proof -
    have "atom x ♯ G'"  using check_branch_s_branchI wf replace_in_g_fresh 
        wfG_dom_supp replace_in_g_wfG by simp
    thus ?thesis using check_branch_s_branchI fresh_prodN by simp
  qed

  moreover have st: "Θ ; Φ ; ℬ ; (x, b_of const, CE_val v  ==  CE_val(V_cons tid cons (V_var x))  AND  c_of const x) #⇩Γ G' ; Δ  ⊢ s ⇐ τ " proof -
    have " wsX ((x, b_of const, CE_val v  ==  CE_val(V_cons tid cons (V_var x))   AND c_of const x) #⇩Γ Γ) xcs" using check_branch_s_branchI wsX_cons2 wsX_fresh wf by force
    moreover have "replace_in_g_subtyped Θ ℬ ((x,  b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x))   AND  c_of const x) #⇩Γ Γ) xcs ((x,  b_of const, CE_val v  ==  CE_val(V_cons tid cons (V_var x)) AND  c_of const x) #⇩Γ G' )" 
      using replace_in_g_subtyped_cons wsX_fresh wf check_branch_s_branchI wfcons by auto
    thus ?thesis using check_branch_s_branchI  calculation by meson
  qed
  moreover have wft: " wfT Θ ℬ G' τ " using
      check_branch_s_branchI ctx_subtype_subtype_rigs subtype_reflI2 subtype_wf by metis
  moreover have "wfD Θ ℬ G' Δ" using check_branch_s_branchI wfD_rig by presburger
  ultimately show ?case using 
      Typing.check_branch_s_branchI 
    using check_branch_s_branchI.hyps by simp

next
  case (check_ifI z Θ Φ ℬ Γ Δ v s1 s2 τ)
  hence wf:"wfG Θ ℬ Γ" using check_s_wf by presburger
  show ?case proof(rule check_s_check_branch_s_check_branch_list.check_ifI)
    show ‹atom z ♯ (Θ, Φ, ℬ, G', Δ, v, s1, s2, τ)› using fresh_prodN replace_in_g_fresh1 wf check_ifI by auto
    show ‹Θ; ℬ; G'  ⊢ v ⇐ ⦃ z : B_bool  | TRUE ⦄› using ctx_subtype_check_v_rigs_eq check_ifI by presburger
    show ‹ Θ ; Φ ; ℬ ; G' ; Δ  ⊢ s1 ⇐ ⦃ z : b_of τ  | CE_val v  ==  CE_val (V_lit L_true)   IMP  c_of τ z  ⦄› using  check_ifI by auto
    show ‹ Θ ; Φ ; ℬ ; G' ; Δ  ⊢ s2 ⇐ ⦃ z : b_of τ  | CE_val v  ==  CE_val (V_lit L_false)   IMP  c_of τ z  ⦄› using  check_ifI by auto
  qed
next

  case (check_let2I x P Φ ℬ G Δ t s1 τ s2 )
  show ?case proof
    have "wfG P ℬ G" using check_let2I check_s_wf by metis
    show  *: "P ; Φ ; ℬ ; G' ; Δ  ⊢ s1 ⇐t" using check_let2I by blast
    show  "atom x ♯ (P, Φ, ℬ, G', Δ, t, s1, τ)" proof -
      have "wfG P ℬ G'" using check_s_wf * by blast
      hence "atom_dom G = atom_dom G'" using check_let2I rigs_atom_dom_eq by presburger
      moreover have "atom x ♯ G" using check_let2I by auto
      moreover have "wfG P ℬ G" using check_s_wf *  replace_in_g_wfG  check_let2I by simp
      ultimately have "atom x ♯ G'" using wfG_dom_supp fresh_def ‹wfG P ℬ G'› by metis
      thus ?thesis using check_let2I by auto
    qed
    show "P ; Φ ; ℬ ;(x, b_of t, c_of t x) #⇩Γ G' ; Δ  ⊢ s2 ⇐ τ " proof - 
      have "wsX ((x, b_of t, c_of t x) #⇩Γ G) xcs" using check_let2I wsX_cons2  wsX_fresh ‹wfG P ℬ G› by simp
      moreover have "replace_in_g_subtyped P ℬ ((x,  b_of t, c_of t x) #⇩Γ G) xcs ((x,  b_of t, c_of t x) #⇩Γ G')" proof(rule  replace_in_g_subtyped_cons )
        show "replace_in_g_subtyped P ℬ G xcs G'" using check_let2I by auto
        have "atom x ♯ G" using check_let2I by auto
        moreover have "wfT P ℬ G t" using check_let2I check_s_wf by metis

        moreover have "atom x ♯ t" using check_let2I check_s_wf wfT_supp by auto
        ultimately show "wfG P ℬ ((x,  b_of t, c_of t x) #⇩Γ G)" using wfT_wf_cons b_of_c_of_eq[of x t] by auto
        show "x ∉ fst ` set xcs" using check_let2I wsX_fresh ‹wfG P ℬ G› by simp
      qed
      ultimately show ?thesis using check_let2I by presburger
    qed  
  qed
next
  case (check_varI u Θ Φ ℬ Γ Δ τ' v τ s)
  show ?case proof
    have "atom u ♯ G'" unfolding fresh_def
      apply(rule  u_not_in_g , rule replace_in_g_wfG)
      using check_v_wf check_varI by simp+
    thus  ‹atom u ♯ (Θ, Φ, ℬ, G', Δ, τ', v, τ)› unfolding fresh_prodN using check_varI by simp
    show ‹Θ; ℬ; G'  ⊢ v ⇐ τ'› using ctx_subtype_check_v_rigs_eq check_varI by auto
    show ‹ Θ ; Φ ; ℬ ; G' ; (u, τ') #⇩Δ Δ  ⊢ s ⇐ τ› using  check_varI by auto
  qed
next
  case (check_assignI P Φ ℬ G Δ u τ v z τ')
  show ?case proof
    show ‹P  ⊢⇩w⇩f Φ › using  check_assignI by auto
    show ‹P ; ℬ ; G'  ⊢⇩w⇩f Δ ›  using  check_assignI wfD_rig by auto
    show ‹(u, τ) ∈ setD Δ›  using  check_assignI by auto
    show ‹P ; ℬ ; G'  ⊢ v ⇐ τ› using ctx_subtype_check_v_rigs_eq check_assignI by auto
    show ‹P ; ℬ ; G'  ⊢ ⦃ z : B_unit  | TRUE ⦄ ≲ τ'›  using ctx_subtype_subtype_rigs check_assignI by auto
  qed
next
  case (check_whileI Δ G P s1 z s2 τ')
  then show ?case using Typing.check_whileI
    by (meson ctx_subtype_subtype_rigs)
next
  case (check_seqI Δ G P s1 z s2 τ)
  then show ?case 
    using check_s_check_branch_s_check_branch_list.check_seqI by blast
next
  case (check_caseI Θ Φ ℬ Γ Δ tid dclist v cs τ z)
  show ?case proof
    show " Θ ;  Φ ; ℬ ; G' ; Δ ; tid ; dclist ; v ⊢ cs ⇐ τ" using check_caseI ctx_subtype_check_v_rigs_eq by auto
    show "AF_typedef tid dclist ∈ set  Θ" using check_caseI by auto
    show "Θ; ℬ; G'  ⊢ v ⇐ ⦃ z : B_id tid  | TRUE ⦄" using check_caseI ctx_subtype_check_v_rigs_eq by auto
    show "⊢⇩w⇩f Θ " using check_caseI by auto
  qed
next
  case (check_assertI x Θ Φ ℬ Γ Δ c τ s)
  show ?case proof
    have wfG: "Θ; ℬ ⊢⇩w⇩f Γ ∧ Θ; ℬ ⊢⇩w⇩f G'" using check_s_wf check_assertI replace_in_g_wfG wfX_wfY by metis
    hence "atom x ♯ G'" using check_assertI replace_in_g_fresh replace_in_g_wfG  by auto
    thus  ‹atom x ♯ (Θ, Φ, ℬ, G', Δ, c, τ, s)› using check_assertI fresh_prodN by auto
    show ‹ Θ ; Φ ; ℬ ; (x, B_bool, c) #⇩Γ G' ; Δ  ⊢ s ⇐ τ› proof(rule check_assertI(5) )
      show "wsX ((x, B_bool, c) #⇩Γ Γ) xcs" using check_assertI wsX_cons3   by simp
      show "Θ; ℬ  ⊢ (x, B_bool, c) #⇩Γ Γ ⟨ xcs ⟩ ↝ (x, B_bool, c) #⇩Γ G'" proof(rule  replace_in_g_subtyped_cons)
        show ‹ Θ; ℬ  ⊢ Γ ⟨ xcs ⟩ ↝ G'› using check_assertI by auto
        show ‹ Θ; ℬ  ⊢⇩w⇩f (x, B_bool, c) #⇩Γ Γ › using check_assertI check_s_wf by metis
        thus ‹x ∉ fst ` set xcs› using check_assertI wsX_fresh wfG_elims wfX_wfY by metis
      qed
    qed
    show ‹Θ; ℬ; G'  ⊨ c › using check_assertI replace_in_g_valid by auto
    show ‹ Θ; ℬ; G' ⊢⇩w⇩f Δ › using check_assertI wfD_rig by auto
  qed
qed

lemma replace_in_g_subtyped_empty:
  assumes "wfG Θ ℬ (Γ' @ (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ)" 
  shows  "replace_in_g_subtyped Θ ℬ (replace_in_g (Γ' @ (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ) x (c'[z'::=V_var x]⇩c⇩v)) [] (Γ' @ (x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ)"
proof -
  have "replace_in_g (Γ' @ (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ) x (c'[z'::=V_var x]⇩c⇩v) = (Γ' @ (x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ)" 
    using assms proof(induct Γ' rule: Γ_induct)
    case GNil
    then show ?case using replace_in_g.simps by auto
  next
    case (GCons x1 b1 c1 Γ1)
    have "x ∉ fst ` toSet ((x1,b1,c1)#⇩ΓΓ1)"  using GCons wfG_inside_fresh atom_dom.simps dom.simps toSet.simps append_g.simps by fast
    hence "x1 ≠ x" using assms wfG_inside_fresh GCons by force
    hence "((x1,b1,c1) #⇩Γ (Γ1 @ (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ))[x⟼c'[z'::=V_var x]⇩c⇩v] = (x1,b1,c1) #⇩Γ (Γ1 @ (x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ)"
      using replace_in_g.simps GCons wfG_elims append_g.simps by metis
    thus ?case using append_g.simps by simp
  qed
  thus ?thesis using replace_in_g_subtyped_nilI by presburger
qed

lemma ctx_subtype_s:
  fixes  s::s
  assumes "Θ ; Φ ; ℬ ; Γ'@((x,b,c[z::=V_var x]⇩c⇩v)#⇩ΓΓ) ; Δ ⊢ s ⇐ τ" and 
    "Θ; ℬ; Γ ⊢ ⦃ z' : b | c' ⦄ ≲ ⦃ z : b | c ⦄" and 
    "atom x ♯ (z,z',c,c')"
  shows "Θ ; Φ ; ℬ ; Γ'@(x,b,c'[z'::=V_var x]⇩c⇩v)#⇩ΓΓ ; Δ ⊢ s ⇐ τ"
proof - 

  have wf: "wfG Θ ℬ (Γ'@((x,b,c[z::=V_var x]⇩c⇩v)#⇩ΓΓ))" using check_s_wf assms by meson
  hence *:"x ∉ fst ` toSet Γ'" using wfG_inside_fresh by force
  have "wfG Θ ℬ ((x,b,c[z::=V_var x]⇩c⇩v)#⇩ΓΓ)" using wf wfG_suffix by metis
  hence xfg: "atom x ♯ Γ" using wfG_elims by metis
  have "x ≠ z'"  using assms fresh_at_base fresh_prod4 by metis
  hence  a2: "atom x ♯ c'" using assms fresh_prod4 by metis

  have "atom x ♯ (z', c', z, c, Γ)" proof -       
    have "x ≠ z" using assms  using assms fresh_at_base fresh_prod4 by metis
    hence  a1 : "atom x ♯ c" using assms subtype_wf   subtype_wf assms wfT_fresh_c xfg by meson
    thus ?thesis using a1 a2 ‹atom x ♯ (z,z',c,c')› fresh_prod4 fresh_Pair xfg by simp
  qed
  hence wc1:" Θ; ℬ; (x, b, c'[z'::=V_var x]⇩v) #⇩Γ Γ  ⊨ c[z::=V_var x]⇩v"
    using  subtype_valid assms fresh_prodN by metis  

  have vld: "Θ;ℬ ; (Γ'@(x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ) ⊨ c[z::=V_var x]⇩c⇩v" proof - 

    have "toSet ((x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ) ⊆ toSet (Γ'@(x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ)" by auto
    moreover have "wfG Θ ℬ (Γ'@(x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ)" proof -
      have *:"wfT Θ ℬ Γ (⦃ z' : b | c' ⦄)" using subtype_wf assms by meson
      moreover have "atom x ♯ (c',Γ)" using xfg a2 by simp
      ultimately have "wfG Θ ℬ ((x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ)" using wfT_wf_cons_flip  freshers by blast
      thus ?thesis using wfG_replace_inside2 check_s_wf assms  by metis
    qed
    ultimately show ?thesis using wc1 valid_weakening subst_defs by metis
  qed
  hence  wbc: "Θ; ℬ; Γ' @ (x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ  ⊢⇩w⇩f c[z::=V_var x]⇩c⇩v" using valid.simps by auto
  have wbc1: "Θ; ℬ; (x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ  ⊢⇩w⇩f c[z::=V_var x]⇩c⇩v" using wc1 valid.simps subst_defs by auto
  have "wsX  (Γ'@((x,b,c[z::=V_var x]⇩c⇩v)#⇩ΓΓ)) [(x, c'[z'::=V_var x]⇩c⇩v)]" proof 
    show "wsX (Γ' @ (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ) []" using wsX_NilI by auto
    show "atom x ∈ atom_dom (Γ' @ (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ)" by simp
    show "x ∉ fst ` set []" by auto
  qed
  moreover have "replace_in_g_subtyped Θ ℬ (Γ'@((x,b,c[z::=V_var x]⇩c⇩v)#⇩ΓΓ)) [(x, c'[z'::=V_var x]⇩c⇩v)] (Γ'@(x,b,c'[z'::=V_var x]⇩c⇩v)#⇩ΓΓ)" proof
    show "Some (b, c[z::=V_var x]⇩c⇩v) = lookup (Γ' @ (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ) x" using lookup_inside* by auto
    show "Θ; ℬ; replace_in_g (Γ' @ (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ) x (c'[z'::=V_var x]⇩c⇩v)  ⊨ c[z::=V_var x]⇩c⇩v"  using vld replace_in_g_split wf by metis
    show "replace_in_g_subtyped Θ ℬ (replace_in_g (Γ' @ (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ) x (c'[z'::=V_var x]⇩c⇩v)) [] (Γ' @ (x, b, c'[z'::=V_var x]⇩c⇩v) #⇩Γ Γ)" 
      using replace_in_g_subtyped_empty wf by presburger
    show "x ∉ fst ` set []" by auto
    show "Θ; ℬ; Γ' @ (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ  ⊢⇩w⇩f c'[z'::=V_var x]⇩c⇩v" 
    proof(rule wf_weakening)
      show ‹Θ; ℬ; (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ  ⊢⇩w⇩f c'[z'::=[ x ]⇧v]⇩c⇩v ›   using wfC_cons_switch[OF wbc1] wf_weakening(6) check_s_wf assms toSet.simps  by metis 
      show ‹Θ; ℬ  ⊢⇩w⇩f Γ' @ (x, b, c[z::=[ x ]⇧v]⇩c⇩v) #⇩Γ Γ ›   using wfC_cons_switch[OF wbc1] wf_weakening(6) check_s_wf assms toSet.simps  by metis
      show ‹toSet ((x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ) ⊆ toSet (Γ' @ (x, b, c[z::=[ x ]⇧v]⇩c⇩v) #⇩Γ Γ)› using append_g.simps toSet.simps by auto
    qed    
  qed
  ultimately show ?thesis using ctx_subtype_s_rigs(1)[OF assms(1)] by presburger 
qed

end