Impressum TypingL.thy

(*<*)
theory TypingL
  imports Typing RCLogicL "HOL-Eisbach.Eisbach"
begin
  (*>*)

chapter  ‹Typing Lemmas›

section ‹Prelude›

text ‹Needed as the typing elimination rules give us facts for an alpha-equivalent version of a term
 and so need to be able to 'jump back' to a typing judgement for the orginal term›

lemma τ_fresh_c[simp]:
  assumes "atom x ♯ { z : b | c }" and "atom z ♯ x"
  shows "atom x ♯ c"
  using τ.fresh assms fresh_at_base 
  by (simp add: fresh_at_base(2))

lemmas subst_defs = subst_b_b_def subst_b_c_def subst_b_τ_def subst_v_v_def subst_v_c_def subst_v_τ_def

lemma wfT_wfT_if1:
  assumes "wfT Θ B Γ ({ z : b_of t | CE_val v == CE_val (V_lit L_false) IMP c_of t z })" and "atom z ♯ (Γ,t)"
  shows "wfT Θ B Γ t" 
  using assms proof(nominal_induct t avoiding: Γ z rule: τ.strong_induct)
  case (T_refined_type z' b' c')
  show ?case proof(rule wfT_wfT_if)
    show ‹ Θ; B; Γ ⊨_wf { z : b' | [ v ]^ce == [ [ L_false ]^v ]^ce IMP c'[z'::=[ z]^v]_cv } ›
      using T_refined_type b_of.simps c_of.simps subst_defs by metis
    show ‹atom z ♯ (c', Γ)› using T_refined_type fresh_prodN τ_fresh_c by metis
  qed
qed

lemma fresh_u_replace_true:
  fixes bv::bv and Γ::Γ
  assumes "atom bv ♯ Γ' @ (x, b, c) #_\<Gamma> Γ"
  shows "atom bv ♯ Γ' @ (x, b, TRUE) #_\<Gamma> Γ"
  using fresh_append_g fresh_GCons assms fresh_Pair c.fresh(1) by auto

lemma wf_replace_true1:
  fixes Γ::Γ and Φ::Φ and Θ::Θ and  Γ'::Γ and v::v and e::e and c::c and c''::c and c'::c and τ::τ and ts::"(string*τ) list" and Δ::Δ and b'::b and b::b and s::s  
    and ftq::fun_typ_q and ft::fun_typ and ce::ce and td::type_def and cs::branch_s and css::branch_list

shows  "Θ; B; G ⊨_wf v : b' ==> G = Γ' @ (x, b, c) #_\<Gamma> Γ ==> Θ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ⊨_wf v : b'" and
  "Θ; B; G ⊨_wf c'' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ⊨_wf c''" and
  "Θ ; B ⊨_wf G ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; B ⊨_wf Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) " and
  "Θ; B; G ⊨_wf τ ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ⊨_wf τ" and
  "Θ; B; Γ ⊨_wf ts ==> True" and 
  "⊨_wf P ==> True" and
  "Θ ; B ⊨_wf b ==> True" and
  "Θ ; B ; G ⊨_wf ce : b' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ⊨_wf ce : b'" and
  "Θ ⊨_wf td ==> True"
proof(nominal_induct   
    b' and c'' and G and τ and ts and P and b and b' and td 
    arbitrary: Γ Γ'  and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ'
    rule:wfV_wfC_wfG_wfT_wfTs_wfTh_wfB_wfCE_wfTD.strong_induct)
  case (wfB_intI Θ B)
  then show ?case using wf_intros by metis
next
  case (wfB_boolI Θ B)
  then show ?case using wf_intros by metis
next
  case (wfB_unitI Θ B)
  then show ?case using wf_intros by metis
next
  case (wfB_bitvecI Θ B)
  then show ?case using wf_intros by metis
next
  case (wfB_pairI Θ B b1 b2)
  then show ?case using wf_intros by metis
next
  case (wfB_consI Θ s dclist B)
  then show ?case using wf_intros by metis
next
  case (wfB_appI Θ b s bv dclist B)
  then show ?case using wf_intros by metis
next
  case (wfV_varI Θ B Γ'' b' c x')
  hence wfg: ‹ Θ ; B ⊨_wf Γ' @ (x, b, TRUE) #_\Γ Γ › by auto
  show ?case proof(cases "x=x'")
    case True
    hence "Some (b, TRUE) = lookup (Γ' @ (x, b, TRUE) #_\<Gamma> Γ) x'" using lookup.simps lookup_inside_wf wfg by simp
    thus ?thesis using Wellformed.wfV_varI[OF wfg] 
      by (metis True lookup_inside_wf old.prod.inject option.inject wfV_varI.hyps(1) wfV_varI.hyps(3) wfV_varI.prems)        
  next
    case False
    hence "Some (b', c) = lookup (Γ' @ (x, b, TRUE) #_\<Gamma> Γ) x'" using  lookup_inside2  wfV_varI by metis
    then show ?thesis using Wellformed.wfV_varI[OF wfg]                                     
      by (metis wfG_elim2 wfG_suffix wfV_varI.hyps(1) wfV_varI.hyps(2) wfV_varI.hyps(3) 
          wfV_varI.prems Wellformed.wfV_varI wf_replace_inside(1))
  qed
next
  case (wfV_litI Θ B Γ l)
  then show ?case using wf_intros using wf_intros by metis
next
  case (wfV_pairI Θ B Γ v1 b1 v2 b2)
  then show ?case using wf_intros by metis
next
  case (wfV_consI s dclist Θ dc x b' c B Γ v)
  then show ?case using wf_intros by metis
next
  case (wfV_conspI s bv dclist Θ dc xc bc cc B b' Γ'' v)
  show ?case proof 
    show ‹AF_typedef_poly s bv dclist ∈ set Θ› using wfV_conspI by metis
    show ‹(dc, { xc : bc | cc }) ∈ set dclist›  using wfV_conspI by metis
    show ‹ Θ ;B ⊨_wf b' ›  using wfV_conspI by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf v : bc[bv::=b']_bb ›  using wfV_conspI by metis
    have "atom bv ♯ Γ' @ (x, b, TRUE) #_\<Gamma> Γ" using fresh_u_replace_true wfV_conspI by metis
    thus  ‹atom bv ♯ (Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, b', v)›  using wfV_conspI fresh_prodN by metis
  qed
next
  case (wfCE_valI Θ B Γ v b)
  then show ?case using wf_intros by metis
next
  case (wfCE_plusI Θ B Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_leqI Θ B Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_eqI Θ B Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_fstI Θ B Γ v1 b1 b2)
  then show ?case using wf_intros by metis
next
  case (wfCE_sndI Θ B Γ v1 b1 b2)
  then show ?case using wf_intros by metis
next
  case (wfCE_concatI Θ B Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_lenI Θ B Γ v1)
  then show ?case using wf_intros by metis
next
  case (wfTI z Θ B Γ''  b' c')
  show ?case proof
    show ‹atom z ♯ (Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ)›  using wfTI fresh_append_g fresh_GCons fresh_prodN  by auto
    show ‹ Θ ; B ⊨_wf b' › using wfTI by metis
    show ‹ Θ; B; (z, b', TRUE) #_\Γ Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf c' ›  using wfTI append_g.simps by metis
  qed
next
  case (wfC_eqI Θ B Γ e1 b e2)
  then show ?case using wf_intros by metis
next
  case (wfC_trueI Θ B Γ)
  then show ?case using wf_intros by metis
next
  case (wfC_falseI Θ B Γ)
  then show ?case using wf_intros by metis
next
  case (wfC_conjI Θ B Γ c1 c2)
  then show ?case using wf_intros by metis
next
  case (wfC_disjI Θ B Γ c1 c2)
  then show ?case using wf_intros by metis
next
  case (wfC_notI Θ B Γ c1)
  then show ?case using wf_intros by metis
next
  case (wfC_impI Θ B Γ c1 c2)
  then show ?case using wf_intros by metis
next
  case (wfG_nilI Θ B)
  then show ?case  using GNil_append by blast
next
  case (wfG_cons1I c Θ B Γ'' x b)
  then show ?case using wf_intros wfG_cons_TRUE2 wfG_elims(2) wfG_replace_inside wfG_suffix
    by (metis (no_types, lifting))
next
  case (wfG_cons2I c Θ B Γ'' x' b)
  then show ?case using wf_intros 
    by (metis wfG_cons_TRUE2 wfG_elims(2) wfG_replace_inside wfG_suffix)
next
  case wfTh_emptyI
  then show ?case  using wf_intros by metis
next
  case (wfTh_consI tdef Θ)
  then show ?case  using wf_intros by metis
next
  case (wfTD_simpleI Θ lst s)
  then show ?case  using wf_intros by metis
next
  case (wfTD_poly Θ bv lst s)
  then show ?case  using wf_intros by metis
next
  case (wfTs_nil Θ B Γ)
  then show ?case  using wf_intros by metis
next
  case (wfTs_cons Θ B Γ τ dc ts)
  then show ?case  using wf_intros by metis
qed

lemma wf_replace_true2:
  fixes Γ::Γ and Φ::Φ and Θ::Θ and  Γ'::Γ and v::v and e::e and c::c and c''::c and c'::c and τ::τ and ts::"(string*τ) list" and Δ::Δ and b'::b and b::b and s::s  
    and ftq::fun_typ_q and ft::fun_typ and ce::ce and td::type_def and cs::branch_s and css::branch_list

shows   "Θ ; Φ ; B ; G ; D ⊨_wf e : b' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; Φ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ); D ⊨_wf e : b'" and
  "Θ ; Φ ; B ; G ; Δ ⊨_wf s : b' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; Φ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ; Δ ⊨_wf s : b'" and
  "Θ ; Φ ; B ; G ; Δ ; tid ; dc ; t ⊨_wf cs : b' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; Φ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ; Δ ; tid ; dc ; t ⊨_wf cs : b'" and
  "Θ ; Φ ; B ; G ; Δ ; tid ; dclist ⊨_wf css : b' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; Φ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ; Δ ; tid ; dclist ⊨_wf css : b'" and

"Θ ⊨_wf Φ ==> True" and
"Θ; B; G ⊨_wf Δ ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ⊨_wf Δ" and

"Θ ; Φ ⊨_wf ftq ==> True" and
"Θ ; Φ ; B ⊨_wf ft ==> True"
proof(nominal_induct   
    b' and b' and b' and b' and Φ and Δ and ftq and ft 
    arbitrary: Γ Γ'  and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ'
    rule:wfE_wfS_wfCS_wfCSS_wfPhi_wfD_wfFTQ_wfFT.strong_induct)

  case (wfE_valI Θ Φ B Γ Δ v b)
  then show ?case using wf_intros using wf_intros wf_replace_true1 by metis
next
  case (wfE_plusI Θ Φ B Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_leqI Θ Φ B Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_eqI Θ Φ B Γ Δ v1 b v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_fstI Θ Φ B Γ Δ v1 b1 b2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_sndI Θ Φ B Γ Δ v1 b1 b2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_concatI Θ Φ B Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_splitI Θ Φ B Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_lenI Θ Φ B Γ Δ v1)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_appI Θ Φ B Γ Δ f x b c τ s v)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_appPI Θ Φ B Γ'' Δ b' bv v τ f x1 b1 c1 s)
  show ?case proof
    show ‹ Θ ⊨_wf Φ › using wfE_appPI wf_replace_true1 by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf Δ › using wfE_appPI by metis
    show ‹ Θ ; B ⊨_wf b' › using wfE_appPI by metis
    have "atom bv ♯ Γ' @ (x, b, TRUE) #_\<Gamma> Γ" using fresh_u_replace_true wfE_appPI fresh_prodN by metis
    thus  ‹atom bv ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, Δ, b', v, (b_of τ)[bv::=b']_b)›
      using wfE_appPI fresh_prodN by auto
    show ‹Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x1 b1 c1 τ s))) = lookup_fun Φ f› using wfE_appPI by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf v : b1[bv::=b']_b › using wfE_appPI wf_replace_true1 by metis
  qed
next
  case (wfE_mvarI Θ Φ B Γ Δ u τ)
  then show ?case using wf_intros wf_replace_true1 by metis
next

  case (wfS_valI Θ Φ B Γ v b Δ)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfS_letI  Θ Φ B Γ'' Δ e b' x1 s b1)
  show ?case proof 
    show ‹ Θ ; Φ ; B ; Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf e : b' › using wfS_letI wf_replace_true1 by metis
    have  ‹ Θ ; Φ ; B ; ((x1, b', TRUE) #_\Γ Γ') @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b1 › apply(rule  wfS_letI(4))
      using wfS_letI  append_g.simps by simp
    thus  ‹ Θ ; Φ ; B ; (x1, b', TRUE) #_\Γ Γ'@ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b1 › using append_g.simps by auto
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf Δ › using wfS_letI by metis
    show "atom x1 ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\<Gamma> Γ, Δ, e, b1)" using fresh_append_g fresh_GCons fresh_prodN wfS_letI by auto
  qed
next
  case (wfS_assertI Θ Φ B x' c Γ'' Δ s b')
  show ?case proof
    show ‹ Θ ; Φ ; B ; (x', B_bool, c) #_\Γ Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b' ›
      using wfS_assertI (2)[of "(x', B_bool, c) #_\<Gamma> Γ'" Γ] wfS_assertI by simp
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf c › using wfS_assertI wf_replace_true1 by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf Δ › using wfS_assertI by metis    
    show  ‹atom x' ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, Δ, c, b', s)› using wfS_assertI fresh_prodN by simp
  qed
next
  case (wfS_let2I  Θ Φ B Γ'' Δ s1 τ  x' s2 ba')
  show ?case proof
    show ‹ Θ ; Φ ; B ; Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s1 : b_of τ › using wfS_let2I wf_replace_true1 by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf τ ›  using wfS_let2I wf_replace_true1 by metis
    have  ‹ Θ ; Φ ; B ; ((x', b_of τ, TRUE) #_\Γ Γ') @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s2 : ba' ›  
      apply(rule wfS_let2I(5))
      using wfS_let2I append_g.simps by auto
    thus ‹ Θ ; Φ ; B ; (x', b_of τ, TRUE) #_\Γ Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s2 : ba' ›  using wfS_let2I append_g.simps by auto
    show ‹atom x' ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, Δ, s1, ba', τ)›   using fresh_append_g fresh_GCons fresh_prodN wfS_let2I by auto
  qed
next
  case (wfS_ifI Θ B Γ v Φ Δ s1 b s2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfS_varI Θ B Γ'' τ v u Φ Δ  b' s)
  show ?case proof
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf τ › using wfS_varI wf_replace_true1 by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf v : b_of τ ›  using wfS_varI wf_replace_true1 by metis
    show ‹atom u ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, Δ, τ, v, b')›  using wfS_varI u_fresh_g fresh_prodN by auto
    show ‹ Θ ; Φ ; B ; Γ' @ (x, b, TRUE) #_\Γ Γ ; (u, τ) #_\Δ Δ ⊨_wf s : b' ›  using wfS_varI by metis
  qed

next
  case (wfS_assignI u τ Δ Θ B Γ Φ v)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfS_whileI Θ Φ B Γ Δ s1 s2 b)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfS_seqI Θ Φ B Γ Δ s1 s2 b)
  then show ?case using wf_intros by metis
next
  case (wfS_matchI Θ B Γ'' v tid dclist Δ Φ cs b')
  show ?case proof
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf v : B_id tid › using wfS_matchI wf_replace_true1 by auto
    show ‹AF_typedef tid dclist ∈ set Θ› using wfS_matchI by auto
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf Δ › using wfS_matchI by auto
    show ‹ Θ ⊨_wf Φ › using wfS_matchI by auto
    show ‹ Θ ; Φ ; B ; Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ; tid ; dclist ⊨_wf cs : b' › using wfS_matchI by auto
  qed
next
  case (wfS_branchI Θ Φ B x' τ Γ'' Δ s b' tid dc)
  show ?case proof
    have ‹ Θ ; Φ ; B ; ((x', b_of τ, TRUE) #_\Γ Γ') @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b' › using wfS_branchI append_g.simps by metis
    thus  ‹ Θ ; Φ ; B ; (x', b_of τ, TRUE) #_\Γ Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b' › using wfS_branchI append_g.simps append_g.simps by metis
    show ‹atom x' ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, Δ, Γ' @ (x, b, TRUE) #_\Γ Γ, τ)› using wfS_branchI by auto
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf Δ › using wfS_branchI by auto
  qed
next
  case (wfS_finalI Θ Φ B Γ Δ tid dc t cs b)
  then show ?case using wf_intros by metis
next
  case (wfS_cons Θ Φ B Γ Δ tid dc t cs b dclist css)
  then show ?case using wf_intros by metis
next
  case (wfD_emptyI Θ B Γ)
  then show ?case  using wf_intros wf_replace_true1 by metis
next
  case (wfD_cons Θ B Γ Δ τ u)
  then show ?case  using wf_intros wf_replace_true1 by metis
next
  case (wfPhi_emptyI Θ)
  then show ?case  using wf_intros by metis
next
  case (wfPhi_consI f Θ Φ ft)
  then show ?case  using wf_intros by metis
next
  case (wfFTNone Θ Φ ft)
  then show ?case  using wf_intros by metis
next
  case (wfFTSome Θ Φ bv ft)
  then show ?case  using wf_intros by metis
next
  case (wfFTI Θ B b Φ x c s τ)
  then show ?case  using wf_intros by metis
qed

lemmas wf_replace_true = wf_replace_true1 wf_replace_true2

section ‹Subtyping›

lemma subtype_reflI2:
  fixes τ::τ
  assumes  "Θ; B; Γ ⊨_wf τ"
  shows "Θ; B; Γ ⊨ τ < τ"
proof -
  obtain z b c where *:"τ = { z : b | c } ∧ atom z ♯ (Θ,B,Γ) ∧ Θ; B; (z, b, TRUE) #_\<Gamma> Γ ⊨_wf c" 
    using  wfT_elims(1)[OF assms] by metis
  obtain x::x where **: "atom x ♯ (Θ, B, Γ, c, z ,c, z , c )" using obtain_fresh by metis
  have "Θ; B; Γ ⊨ { z : b | c } < { z : b | c }" proof
    show "Θ; B; Γ ⊨_wf { z : b | c }" using * assms by auto
    show "Θ; B; Γ ⊨_wf { z : b | c }" using * assms by auto
    show "atom x ♯ (Θ, B, Γ, z , c , z , c )" using fresh_prod6 fresh_prod5 ** by metis
    thus  "Θ; B; (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ ⊨ c[z::=V_var x]_v " using wfT_wfC_cons assms * ** subst_v_c_def  by simp
  qed
  thus ?thesis using * by auto
qed

lemma subtype_reflI:  
  assumes "{ z1 : b | c1 } = { z2 : b | c2 }" and wf1: "Θ; B;Γ ⊨_wf ({ z1 : b | c1 })"
  shows "Θ; B; Γ ⊨ ({ z1 : b | c1 }) < ({ z2 : b | c2 })"
  using assms subtype_reflI2 by metis

nominal_function base_eq :: "Γ ==> τ ==> τ ==> bool" where
  "base_eq _ { z1 : b1| c1 } { z2 : b2 | c2 } = (b1 = b2)" 
  apply(auto,simp add: eqvt_def base_eq_graph_aux_def )
  by (meson τ.exhaust)
nominal_termination (eqvt)  by lexicographic_order

lemma subtype_wfT:
  fixes t1::τ and t2::τ
  assumes "Θ; B; Γ ⊨ t1 < t2" 
  shows "Θ; B; Γ ⊨_wf t1 ∧ Θ; B; Γ ⊨_wf t2"
  using assms subtype_elims by metis

lemma  subtype_eq_base:
  assumes "Θ; B; Γ ⊨ ({ z1 : b1| c1 }) < ({ z2 : b2 | c2 })"
  shows "b1=b2"
  using subtype.simps  assms by auto

lemma subtype_eq_base2: 
  assumes "Θ; B; Γ ⊨ t1 < t2"
  shows "b_of t1 = b_of t2"
  using assms proof(rule  subtype.induct[of Θ  B Γ t1 t2],goal_cases)
  case (1 Θ  Γ z1 b c1 z2 c2 x)
  then show ?case using subtype_eq_base by auto
qed

lemma  subtype_wf: 
  fixes τ1::τ and τ2::τ
  assumes "Θ; B; Γ ⊨ τ1 < τ2" 
  shows "Θ; B; Γ ⊨_wf τ1 ∧Θ; B; Γ ⊨_wf τ2"
  using assms
proof(rule  subtype.induct[of Θ B Γ τ1 τ2],goal_cases)
  case (1 Θ  ΓG z1 b c1 z2 c2 x)
  then show ?case by blast
qed

lemma  subtype_g_wf: 
  fixes τ1::τ and τ2::τ and Γ::Γ
  assumes "Θ; B; Γ ⊨ τ1 < τ2" 
  shows "Θ ; B⊨_wf Γ"
  using assms
proof(rule  subtype.induct[of Θ B Γ τ1 τ2],goal_cases)
  case (1 Θ B Γ z1 b c1 z2 c2 x)
  then show ?case using wfX_wfY by auto
qed

text ‹ For when we have a particular y that satisfies the freshness conditions that we want the validity check to use ›

lemma valid_flip_simple: 
  assumes "Θ; B; (z, b, c) #_\<Gamma> Γ ⊨ c'" and  "atom z ♯ Γ" and "atom x ♯ (z, c, z, c', Γ)"
  shows "Θ; B; (x, b, (z ↔ x ) ∙ c) #_\<Gamma> Γ ⊨ (z ↔ x ) ∙ c'"
proof -
  have "(z ↔ x ) ∙ Θ; B; (z ↔ x ) ∙ ((z, b, c) #_\<Gamma> Γ) ⊨ (z ↔ x ) ∙ c'"
    using True_eqvt valid.eqvt assms beta_flip_eq wfX_wfY by metis
  moreover have " ⊨_wf Θ" using valid.simps wfC_wf wfG_wf assms by metis
  ultimately show ?thesis 
    using theta_flip_eq G_cons_flip_fresh3[of x Γ z b c]  assms fresh_Pair flip_commute by metis
qed

lemma valid_wf_all:
  assumes " Θ; B; (z0,b,c0)#_\<Gamma>G ⊨ c"   
  shows "wfG Θ B G" and "wfC Θ B ((z0,b,c0)#_\<Gamma>G) c" and "atom z0 ♯ G"
  using valid.simps wfC_wf wfG_cons assms by metis+

lemma valid_wfT: 
  fixes z::x
  assumes " Θ; B; (z0,b,c0[z::=V_var z0]_v)#_\<Gamma>G ⊨ c[z::=V_var z0]_v" and "atom z0 ♯ (Θ, B, G,c,c0)"
  shows "Θ; B; G ⊨_wf { z : b | c0 }"    and  "Θ; B; G ⊨_wf { z : b | c }"
proof -
  have "atom z0 ♯ c0" using assms fresh_Pair by auto
  moreover have *:" Θ ; B ⊨_wf (z0,b,c0[z::=V_var z0]_cv)#_\<Gamma>G" using valid_wf_all wfX_wfY assms subst_v_c_def by metis
  ultimately show wft: "Θ; B; G ⊨_wf { z : b | c0 }"  using wfG_wfT[OF *] by auto

  have "atom z0 ♯ c" using assms fresh_Pair by auto
  moreover have wfc: "Θ; B; (z0,b,c0[z::=V_var z0]_v)#_\<Gamma>G ⊨_wf c[z::=V_var z0]_v" using valid_wf_all assms by metis
  have  "Θ; B; G ⊨_wf { z0 : b | c[z::=V_var z0]_v }" proof
    show ‹atom z0 ♯ (Θ, B, G)› using assms fresh_prodN by simp
    show ‹ Θ ; B ⊨_wf b › using wft wfT_wfB by force
    show ‹ Θ; B; (z0, b, TRUE) #_\Γ G ⊨_wf c[z::=[ z0 ]^v]_v › using wfc wfC_replace_inside[OF wfc, of GNil z0 b "c0[z::=[ z0 ]^v]_v" G C_true] wfC_trueI 
        append_g.simps 
      by (metis "local.*" wfG_elim2 wf_trans(2))
  qed
  moreover have "{ z0 : b | c[z::=V_var z0]_v } = { z : b | c }" using ‹atom z0 ♯ c0› τ.eq_iff  Abs1_eq_iff(3) 
    using calculation(1) subst_v_c_def by auto
  ultimately show   "Θ; B; G ⊨_wf { z : b | c }" by auto
qed

lemma valid_flip: 
  fixes c::c and z::x and z0::x and xx2::x
  assumes " Θ; B; (xx2, b, c0[z0::=V_var xx2]_v) #_\<Gamma> Γ ⊨ c[z::=V_var xx2]_v" and 
    "atom xx2 ♯ (c0,Γ,c,z) " and "atom z0 ♯ (Γ,c,z)"
  shows " Θ; B; (z0, b, c0) #_\<Gamma> Γ ⊨ c[z::=V_var z0]_v"
proof -

  have " ⊨_wf Θ" using assms valid_wf_all wfX_wfY by metis
  hence " Θ ; B ; (xx2 ↔ z0 ) ∙ ((xx2, b, c0[z0::=V_var xx2]_v) #_\<Gamma> Γ) ⊨ ((xx2 ↔ z0 ) ∙ c[z::=V_var xx2]_v)"
    using valid.eqvt True_eqvt assms beta_flip_eq theta_flip_eq by metis
  hence " Θ; B; (((xx2 ↔ z0 ) ∙ xx2, b, (xx2 ↔ z0 ) ∙ c0[z0::=V_var xx2]_v) #_\<Gamma> (xx2 ↔ z0 ) ∙ Γ) ⊨ ((xx2 ↔ z0 ) ∙(c[z::=V_var xx2]_v))"
    using G_cons_flip[of xx2 z0 xx2 b "c0[z0::=V_var xx2]_v" Γ] by auto
  moreover have "(xx2 ↔ z0 ) ∙ xx2 = z0" by simp
  moreover have "(xx2 ↔ z0 ) ∙ c0[z0::=V_var xx2]_v = c0" 
    using assms subst_cv_v_flip[of xx2 c0 z0 "V_var z0"] assms fresh_prod4 by auto
  moreover have "(xx2 ↔ z0 ) ∙ Γ = Γ" proof -  
    have "atom xx2 ♯ Γ" using assms by auto
    moreover have "atom z0 ♯ Γ" using assms by auto
    ultimately show ?thesis using flip_fresh_fresh by auto
  qed
  moreover have "(xx2 ↔ z0 ) ∙ (c[z::=V_var xx2]_v) =c[z::=V_var z0]_v" 
    using subst_cv_v_flip3 assms by simp
  ultimately show ?thesis by auto
qed

lemma subtype_valid:
  assumes "Θ; B; Γ ⊨ t1 < t2" and "atom y ♯ Γ" and "t1 = { z1 : b | c1 }" and "t2 = { z2 : b | c2 }"
  shows  "Θ; B; ((y, b, c1[z1::=V_var y]_v) #_\<Gamma> Γ) ⊨ c2[z2::=V_var y]_v"
  using assms proof(nominal_induct t2 avoiding: y rule: subtype.strong_induct)
  case (subtype_baseI x Θ B Γ z c z' c' ba)

  hence "(x ↔ y) ∙ Θ ; (x ↔ y) ∙ B ; (x ↔ y) ∙ ((x, ba, c[z::=[ x ]^v]_v) #_\<Gamma> Γ) ⊨ (x ↔ y) ∙ c'[z'::=[ x ]^v]_v" using valid.eqvt 
    using permute_boolI by blast
  moreover have  " ⊨_wf Θ" using valid.simps wfC_wf wfG_wf subtype_baseI by metis
  ultimately have  "Θ; B; ((y, ba, (x ↔ y) ∙ c[z::=[ x ]^v]_v) #_\<Gamma> Γ) ⊨ (x ↔ y) ∙ c'[z'::=[ x ]^v]_v" 
    using subtype_baseI theta_flip_eq beta_flip_eq τ.eq_iff  G_cons_flip_fresh3[of y Γ x ba]  by (metis flip_commute)
  moreover have "(x ↔ y) ∙ c[z::=[ x ]^v]_v = c1[z1::=[ y ]^v]_v" 
    by (metis subtype_baseI permute_flip_cancel subst_cv_id subst_cv_v_flip3 subst_cv_var_flip type_eq_subst_eq wfT_fresh_c subst_v_c_def)
  moreover have  "(x ↔ y) ∙ c'[z'::=[ x ]^v]_v = c2[z2::=[ y ]^v]_v" 
    by (metis subtype_baseI permute_flip_cancel subst_cv_id subst_cv_v_flip3 subst_cv_var_flip type_eq_subst_eq wfT_fresh_c subst_v_c_def)

  ultimately show ?case using subtype_baseI τ.eq_iff by metis
qed

lemma subtype_valid_simple:
  assumes "Θ; B; Γ ⊨ t1 < t2" and "atom z ♯ Γ" and "t1 = { z : b | c1 }" and "t2 = { z : b | c2 }"
  shows  "Θ; B; ((z, b, c1) #_\<Gamma> Γ) ⊨ c2"
  using subst_v_c_def subst_v_id assms subtype_valid[OF assms] by simp

lemma obtain_for_t_with_fresh:
  assumes "atom x ♯ t"
  shows "∃b c. t = { x : b | c }"
proof -
  obtain z1 b1 c1 where *:" t = { z1 : b1 | c1 } ∧ atom z1 ♯ t" using obtain_fresh_z by metis
  then have "t = (x ↔ z1) ∙ t" using flip_fresh_fresh assms by metis
  also have "... = { (x ↔ z1) ∙ z1 : (x ↔ z1) ∙ b1 | (x ↔ z1) ∙ c1 }" using * assms by simp
  also have "... = { x : b1 | (x ↔ z1) ∙ c1 }" using * assms by auto
  finally show ?thesis by auto
qed

lemma subtype_trans: 
  assumes "Θ; B; Γ ⊨ τ1 < τ2" and "Θ; B; Γ ⊨ τ2 < τ3"
  shows "Θ; B; Γ ⊨ τ1 < τ3"
  using assms proof(nominal_induct  avoiding: τ3 rule: subtype.strong_induct)
  case (subtype_baseI x Θ B Γ z c z' c' b)
  hence "b_of τ3 = b" using  subtype_eq_base2 b_of.simps by metis
  then obtain z'' c'' where t3: "τ3 = { z'' : b | c''} ∧ atom z'' ♯ x" 
    using obtain_fresh_z2 by metis
  hence xf: "atom x ♯ (z'', c'')" using fresh_prodN subtype_baseI τ.fresh by auto
  have "Θ; B; Γ ⊨ { z : b | c } < { z'' : b | c''}" 
  proof(rule Typing.subtype_baseI)
    show ‹atom x ♯ (Θ, B, Γ, z, c, z'', c'')› using t3 fresh_prodN subtype_baseI xf by simp
    show ‹ Θ; B; Γ ⊨_wf { z : b | c } › using subtype_baseI by auto
    show ‹ Θ; B; Γ ⊨_wf { z'' : b | c'' } › using subtype_baseI t3 subtype_elims by metis
    have " Θ; B; (x, b, c'[z'::=[ x ]^v]_v) #_\<Gamma> Γ ⊨ c''[z''::=[ x ]^v]_v "
      using subtype_valid[OF ‹Θ; B; Γ ⊨ { z' : b | c' } < τ3› , of x z' b c' z'' c''] subtype_baseI 
        t3 by simp
    thus ‹Θ; B; (x, b, c[z::=[ x ]^v]_v) #_\Γ Γ ⊨ c''[z''::=[ x ]^v]_v ›
      using  valid_trans_full[of Θ B x b c z Γ c' z' c'' z'' ] subtype_baseI  t3 by simp
  qed
  thus ?case using t3 by simp
qed

lemma subtype_eq_e:
  assumes "∀i s1 s2 G. wfG P B G ∧ wfI P G i ∧ eval_e i e1 s1 ∧ eval_e i e2 s2 ⟶ s1 = s2"   and "atom z1 ♯ e1" and "atom z2 ♯ e2" and "atom z1 ♯ Γ" and "atom z2 ♯ Γ"
    and "wfCE P B Γ e1 b" and "wfCE P B Γ e2 b" 
  shows "P; B; Γ ⊨ { z1 : b | CE_val (V_var z1) == e1 } < ({ z2 : b | CE_val (V_var z2) == e2 })"
proof -

  have "wfCE P B Γ e1 b" and "wfCE P B Γ e2 b" using  assms by auto

  have wst1: "wfT P B Γ ({ z1 : b | CE_val (V_var z1) == e1 })" 
    using wfC_e_eq  wfTI assms wfX_wfB wfG_fresh_x 
    by (simp add: wfT_e_eq)

  moreover have wst2:"wfT P B Γ ({ z2 : b | CE_val (V_var z2) == e2 })" 
    using wfC_e_eq wfX_wfB wfTI assms wfG_fresh_x 
    by (simp add: wfT_e_eq)

  moreover obtain x::x where xf: "atom x ♯ (P, B , z1, CE_val (V_var z1) == e1 , z2, CE_val (V_var z2) == e2 , Γ)" using obtain_fresh by blast
  moreover have vld: "P; B ; (x, b, (CE_val (V_var z1) == e1 )[z1::=V_var x]_v) #_\<Gamma> Γ ⊨ (CE_val (V_var z2) == e2 )[z2::=V_var x]_v "  (is "P; B ; ?G ⊨ ?c")
  proof -

    have wbg: "P; B ⊨_wf ?G ∧ P ; B ⊨_wf Γ ∧ toSet Γ ⊆ toSet ?G"  proof -        
      have "P; B ⊨_wf ?G"  proof(rule wfG_consI) 
        show "P; B ⊨_wf Γ" using assms wfX_wfY by metis
        show "atom x ♯ Γ" using xf by auto
        show "P; B ⊨_wf b " using assms(6) wfX_wfB by auto
        show "P; B ; (x, b, TRUE) #_\<Gamma> Γ ⊨_wf (CE_val (V_var z1) == e1 )[z1::=V_var x]_v " 
          using wfC_e_eq[OF assms(6)] wf_subst(2)
          by (simp add: ‹atom x ♯ Γ› assms(2) subst_v_c_def)
      qed
      moreover hence  "P; B ⊨_wf Γ" using wfG_elims by metis
      ultimately show ?thesis using toSet.simps by auto 
    qed

    have wsc: "wfC P B ?G ?c" proof -
      have "wfCE P B ?G (CE_val (V_var x)) b" proof      
        show ‹ P; B ; (x, b, (CE_val (V_var z1) == e1 )[z1::=V_var x]_v) #_\Γ Γ ⊨_wf V_var x : b › using wfV_varI lookup.simps wbg by auto
      qed
      moreover have "wfCE P B ?G e2 b" using wf_weakening assms wbg by metis
      ultimately have "wfC P B ?G (CE_val (V_var x) == e2 )" using wfC_eqI by simp
      thus ?thesis using subst_cv.simps(6) ‹atom z2 ♯ e2› subst_v_c_def by simp
    qed

    moreover have "∀i. wfI P ?G i ∧ is_satis_g i ?G ⟶ is_satis i ?c" proof(rule allI , rule impI)
      fix i
      assume as: "wfI P ?G i ∧ is_satis_g i ?G" 
      hence "is_satis i ((CE_val (V_var z1) == e1 )[z1::=V_var x]_v)" 
        by (simp add: is_satis_g.simps(2))
      hence "is_satis i (CE_val (V_var x) == e1 )" using subst_cv.simps assms subst_v_c_def by auto
      then obtain s1 and s2 where *:"eval_e i (CE_val (V_var x)) s1 ∧ eval_e i e1 s2 ∧ s1=s2" using is_satis.simps eval_c_elims by metis
      moreover hence "eval_e i e2 s1" proof -
        have **:"wfI P ?G i" using as by auto
        moreover have "wfCE P B ?G e1 b ∧ wfCE P B ?G e2 b" using assms xf wf_weakening wbg by metis
        moreover then  obtain s2' where "eval_e i e2 s2'" using assms wfI_wfCE_eval_e ** by metis
        ultimately show ?thesis using * assms(1) wfX_wfY by metis
      qed
      ultimately have  "is_satis i (CE_val (V_var x) == e2 )" using is_satis.simps eval_c_eqI by force
      thus "is_satis i ((CE_val (V_var z2) == e2 )[z2::=V_var x]_v)"  using is_satis.simps eval_c_eqI assms subst_cv.simps subst_v_c_def by auto
    qed
    ultimately show ?thesis using valid.simps by simp
  qed
  moreover have "atom x ♯ (P, B, Γ, z1 , CE_val (V_var z1) == e1, z2, CE_val (V_var z2) == e2 ) " 
    unfolding fresh_prodN using  xf fresh_prod7 τ.fresh by fast
  ultimately show ?thesis using subtype_baseI[OF _ wst1 wst2  vld] xf by simp
qed

lemma subtype_eq_e_nil:
  assumes  "∀i s1 s2 G. wfG P B G ∧ wfI P G i ∧ eval_e i e1 s1 ∧ eval_e i e2 s2 ⟶ s1 = s2" and "supp e1 = {}" and "supp e2 = {}" and "wfTh P" 
    and "wfCE P B GNil e1 b" and "wfCE P B GNil e2 b"  and "atom z1 ♯ GNil" and "atom z2 ♯ GNil"
  shows "P; B ; GNil ⊨ { z1 : b | CE_val (V_var z1) == e1 } < ({ z2 : b | CE_val (V_var z2) == e2 })"
  apply(rule subtype_eq_e,auto simp add: assms e.fresh)
  using  assms fresh_def e.fresh  supp_GNil by metis+

lemma subtype_gnil_fst_aux:
  assumes "supp v₁ = {}" and "supp (V_pair v₁ v₂) = {}" and "wfTh P" and "wfCE P B GNil (CE_val v₁) b" and "wfCE P B GNil (CE_fst [V_pair v₁ v₂]^ce) b" and 
    "wfCE P B GNil (CE_val v₂) b2"  and "atom z1 ♯ GNil" and "atom z2 ♯ GNil"
  shows "P; B ; GNil ⊨ ({ z1 : b | CE_val (V_var z1) == CE_val v₁ }) < ({ z2 : b | CE_val (V_var z2) == CE_fst [V_pair v₁ v₂]^ce })"
proof - 
  have "∀i s1 s2 G . wfG P B G ∧ wfI P G i ∧ eval_e i ( CE_val v₁) s1 ∧ eval_e i (CE_fst [V_pair v₁ v₂]^ce) s2 ⟶ s1 = s2" proof(rule+) 
    fix i s1 s2 G
    assume as: "wfG P B G ∧ wfI P G i ∧ eval_e i (CE_val v₁) s1 ∧ eval_e i (CE_fst [V_pair v₁ v₂]^ce) s2"
    hence "wfCE P B G (CE_val v₂) b2" using assms wf_weakening 
      by (metis empty_subsetI toSet.simps(1))
    then obtain s3 where "eval_e i (CE_val v₂) s3" using wfI_wfCE_eval_e as by metis
    hence "eval_v i ((V_pair v₁ v₂)) (SPair s1 s3)"
      by (meson as eval_e_elims(1) eval_v_pairI)
    hence "eval_e i (CE_fst [V_pair v₁ v₂]^ce) s1" using eval_e_fstI eval_e_valI by metis
    show "s1 = s2" using as eval_e_uniqueness
      using ‹eval_e i (CE_fst [V_pair v₁ v₂]^ce) s1› by auto
  qed
  thus ?thesis using subtype_eq_e_nil  ce.supp assms by auto
qed

lemma subtype_gnil_snd_aux:
  assumes "supp v₂ = {}" and "supp (V_pair v₁ v₂) = {}" and "wfTh P" and "wfCE P B GNil (CE_val v₂) b" and 
    "wfCE P B GNil (CE_snd [(V_pair v₁ v₂)]^ce) b" and 
    "wfCE P B GNil (CE_val v₁) b2"  and "atom z1 ♯ GNil" and "atom z2 ♯ GNil"
  shows "P; B ; GNil ⊨ ({ z1 : b | CE_val (V_var z1) == CE_val v₂ }) < ({ z2 : b | CE_val (V_var z2) == CE_snd [(V_pair v₁ v₂)]^ce })"
proof - 
  have "∀i s1 s2 G. wfG P B G ∧ wfI P G i ∧ eval_e i ( CE_val v₂) s1 ∧ eval_e i (CE_snd [(V_pair v₁ v₂)]^ce) s2 ⟶ s1 = s2" proof(rule+) 
    fix i s1 s2 G
    assume as: " wfG P B G ∧ wfI P G i ∧ eval_e i (CE_val v₂) s1 ∧ eval_e i (CE_snd [(V_pair v₁ v₂)]^ce) s2"
    hence "wfCE P B G (CE_val v₁) b2" using assms wf_weakening 
      by (metis empty_subsetI toSet.simps(1))
    then obtain s3 where "eval_e i (CE_val v₁) s3" using wfI_wfCE_eval_e as by metis
    hence "eval_v i ((V_pair v₁ v₂)) (SPair s3 s1)"
      by (meson as eval_e_elims eval_v_pairI)
    hence "eval_e i (CE_snd [(V_pair v₁ v₂)]^ce) s1" using eval_e_sndI eval_e_valI by metis
    show "s1 = s2" using as eval_e_uniqueness
      using ‹eval_e i (CE_snd [V_pair v₁ v₂]^ce) s1› by auto
  qed
  thus ?thesis using assms subtype_eq_e_nil  by (simp add: ce.supp ce.supp)
qed

lemma subtype_gnil_fst:
  assumes "Θ ; {||} ; GNil ⊨_wf [#1[[v₁,v₂]^v]^ce]^ce : b" 
  shows "Θ ; {||} ; GNil ⊨ ({ z₁ : b | [[z₁]^v]^ce == [v₁]^ce }) <
        ({ z₂ : b | [[z₂]^v]^ce == [#1[[v₁, v₂]^v]^ce]^ce })"
proof  -
  obtain b2 where **:" Θ ; {||} ; GNil ⊨_wf V_pair v₁ v₂ : B_pair b b2" using wfCE_elims(4)[OF assms ] wfCE_elims by metis
  obtain b1' b2' where *:"B_pair b b2 = B_pair b1' b2' ∧ Θ ; {||} ; GNil ⊨_wf v₁ : b1' ∧ Θ ; {||} ; GNil ⊨_wf v₂ : b2'" 
    using wfV_elims(3)[OF **] by metis

  show ?thesis proof(rule subtype_gnil_fst_aux)
    show ‹supp v₁ = {}› using * wfV_supp_nil by auto
    show ‹supp (V_pair v₁ v₂) = {}› using ** wfV_supp_nil e.supp by metis
    show ‹⊨_wf Θ› using assms wfX_wfY   by metis
    show ‹Θ; {||}; GNil ⊨_wf CE_val v₁ : b › using  wfCE_valI  "*" by auto
    show ‹Θ; {||}; GNil ⊨_wf CE_fst [V_pair v₁ v₂]^ce : b › using assms by auto
    show ‹Θ; {||}; GNil ⊨_wf CE_val v₂ : b2 ›using  wfCE_valI  "*" by auto
    show ‹atom z₁ ♯ GNil› using fresh_GNil by metis
    show ‹atom z₂ ♯ GNil› using fresh_GNil by metis
  qed
qed

lemma subtype_gnil_snd:
  assumes "wfCE P {||} GNil (CE_snd ([V_pair v₁ v₂]^ce)) b" 
  shows "P ; {||} ; GNil ⊨ ({ z1 : b | CE_val (V_var z1) == CE_val v₂ }) < ({ z2 : b | CE_val (V_var z2) == CE_snd [(V_pair v₁ v₂)]^ce })"
proof  -
  obtain b1 where **:" P ; {||} ; GNil ⊨_wf V_pair v₁ v₂ : B_pair b1 b " using wfCE_elims assms by metis
  obtain b1' b2' where *:"B_pair b1 b = B_pair b1' b2' ∧ P ; {||} ; GNil ⊨_wf v₁ : b1' ∧ P ; {||} ; GNil ⊨_wf v₂ : b2'" using wfV_elims(3)[OF **] by metis

  show ?thesis proof(rule subtype_gnil_snd_aux)
    show ‹supp v₂ = {}› using * wfV_supp_nil by auto
    show ‹supp (V_pair v₁ v₂) = {}› using ** wfV_supp_nil e.supp by metis
    show ‹⊨_wf P› using assms wfX_wfY  by metis
    show ‹P; {||}; GNil ⊨_wf CE_val v₁ : b1 › using wfCE_valI   "*" by simp
    show ‹P; {||}; GNil ⊨_wf CE_snd [(V_pair v₁ v₂)]^ce : b › using assms by auto
    show ‹P; {||}; GNil ⊨_wf CE_val v₂ : b ›using  wfCE_valI  "*" by simp
    show ‹atom z1 ♯ GNil› using fresh_GNil by metis
    show ‹atom z2 ♯ GNil› using fresh_GNil by metis
  qed
qed

lemma subtype_fresh_tau:
  fixes x::x
  assumes "atom x ♯ t1" and "atom x ♯ Γ" and "P; B; Γ ⊨ t1 < t2"
  shows "atom x ♯ t2"
proof -
  have wfg: "P; B ⊨_wf Γ" using subtype_wf wfX_wfY  assms by metis
  have wft: "wfT P B Γ t2" using subtype_wf wfX_wfY assms by blast
  hence "supp t2 ⊆ atom_dom Γ ∪ supp B" using wf_supp 
    using atom_dom.simps by auto
  moreover have "atom x ∉ atom_dom Γ" using ‹atom x ♯ Γ› wfG_atoms_supp_eq wfg fresh_def by blast 
  ultimately show "atom x ♯ t2" using fresh_def
    by (metis Un_iff contra_subsetD x_not_in_b_set)
qed

lemma subtype_if_simp:
  assumes "wfT P B GNil ({ z1 : b | CE_val (V_lit l ) == CE_val (V_lit l) IMP c[z::=V_var z1]_v })" and
    "wfT P B GNil ({ z : b | c })" and "atom z1 ♯ c"
  shows  "P; B ; GNil ⊨ ({ z1 : b | CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v }) < ({ z : b | c })" 
proof -
  obtain x::x where xx: "atom x ♯ ( P , B , z1, CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v , z, c, GNil)" using obtain_fresh_z by blast
  hence xx2: " atom x ♯ (CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v , c, GNil)" using fresh_prod7 fresh_prod3 by fast
  have *:"P; B ; (x, b, (CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v )[z1::=V_var x]_v) #_\<Gamma> GNil ⊨ c[z::=V_var x]_v " (is "P; B ; ?G ⊨ ?c" ) proof -
    have "wfC P B ?G ?c"  using wfT_wfC_cons[OF assms(1) assms(2),of x] xx fresh_prod5 fresh_prod3 subst_v_c_def by metis
    moreover have "(∀i. wfI P ?G i ∧ is_satis_g i ?G ⟶ is_satis i ?c)" proof(rule allI, rule impI)
      fix i
      assume as1: "wfI P ?G i ∧ is_satis_g i ?G" 
      have "((CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v )[z1::=V_var x]_v) = ((CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var x]_v ))" 
        using assms subst_v_c_def by auto
      hence "is_satis i ((CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var x]_v ))" using is_satis_g.simps as1 by presburger
      moreover have "is_satis i ((CE_val (V_lit l) == CE_val (V_lit l)))" using is_satis.simps eval_c_eqI[of i "(CE_val (V_lit l))" "eval_l l"] eval_e_uniqueness 
          eval_e_valI eval_v_litI by metis
      ultimately show  "is_satis i ?c" using  is_satis_mp[of i] by metis
    qed
    ultimately show ?thesis using valid.simps by simp
  qed
  moreover have "atom x ♯ (P, B, GNil, z1 , CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v , z, c )" 
    unfolding fresh_prod5 τ.fresh using xx fresh_prodN x_fresh_b by metis
  ultimately show ?thesis using subtype_baseI assms xx xx2  by metis
qed

lemma subtype_if:
  assumes "P; B; Γ ⊨ { z : b | c } < { z' : b | c' }" and 
    "wfT P B Γ ({ z1 : b | CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v })"  and
    "wfT P B Γ ({ z2 : b | CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v })" and 
    "atom z1 ♯ v" and  "atom z ♯ Γ" and "atom z1 ♯ c" and "atom z2 ♯ c'" and "atom z2 ♯ v"
  shows   "P; B ; Γ ⊨ { z1 : b | CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v } < { z2 : b | CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v }"
proof -
  obtain x::x where xx: "atom x ♯ (P,B,z,c,z', c', z1, CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v , z2, CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v , Γ)" 
    using obtain_fresh_z by blast
  hence xf: "atom x ♯ (z, c, z', c', Γ)" by simp
  have xf2: "atom x ♯ (z1, CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v , z2, CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v , Γ)" 
    using xx fresh_prod4 fresh_prodN by metis

  moreover have "P; B ; (x, b, (CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v )[z1::=V_var x]_v) #_\<Gamma> Γ ⊨ (CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v )[z2::=V_var x]_v" 
    (is "P; B ; ?G ⊨ ?c" )
  proof -
    have wbc: "wfC P B ?G ?c" using  assms xx fresh_prod4 fresh_prod2 wfT_wfC_cons assms subst_v_c_def by metis

    moreover have "∀i. wfI P ?G i ∧ is_satis_g i ?G ⟶ is_satis i ?c" proof(rule allI, rule impI)
      fix i
      assume a1: "wfI P ?G i ∧ is_satis_g i ?G"

      have *: " is_satis i ((CE_val v == CE_val (V_lit l))) ⟶ is_satis i ((c'[z'::=V_var z2]_v )[z2::=V_var x]_v)" 
      proof 
        assume a2: "is_satis i ((CE_val v == CE_val (V_lit l)))" 

        have "is_satis i ((CE_val v == CE_val (V_lit l) IMP (c[z::=V_var z1]_v ))[z1::=V_var x]_v)" 
          using a1 is_satis_g.simps  by simp
        moreover have "((CE_val v == CE_val (V_lit l) IMP (c[z::=V_var z1]_v ))[z1::=V_var x]_v) = (CE_val v == CE_val (V_lit l) IMP ((c[z::=V_var z1]_v )[z1::=V_var x]_v))" 
          using  assms subst_v_c_def by simp
        ultimately have "is_satis i (CE_val v == CE_val (V_lit l) IMP ((c[z::=V_var z1]_v )[z1::=V_var x]_v))" by argo

        hence  "is_satis i ((c[z::=V_var z1]_v )[z1::=V_var x]_v)" using a2 is_satis_mp by auto
        moreover have "((c[z::=V_var z1]_v )[z1::=V_var x]_v) = ((c[z::=V_var x]_v ))" using assms by auto
        ultimately have  "is_satis i ((c[z::=V_var x]_v ))"  using a2 is_satis.simps by auto

        hence "is_satis_g i ((x,b,(c[z::=V_var x]_v )) #_\<Gamma> Γ)" using a1 is_satis_g.simps by meson
        moreover have "wfI P ((x,b,(c[z::=V_var x]_v )) #_\<Gamma> Γ) i" proof -
          obtain s where "Some s = i x ∧ wfRCV P s b ∧ wfI P Γ i" using wfI_def a1 by auto
          thus ?thesis using wfI_def by auto
        qed
        ultimately have  "is_satis i ((c'[z'::=V_var x]_v))" using subtype_valid assms(1) xf valid.simps by simp

        moreover have "(c'[z'::=V_var x]_v) = ((c'[z'::=V_var z2]_v )[z2::=V_var x]_v)" using assms by auto
        ultimately show "is_satis i ((c'[z'::=V_var z2]_v )[z2::=V_var x]_v)" by auto
      qed

      moreover have "?c = ((CE_val v == CE_val (V_lit l)) IMP ((c'[z'::=V_var z2]_v )[z2::=V_var x]_v))" 
        using  assms subst_v_c_def by simp

      moreover have "∃b1 b2. eval_c i (CE_val v == CE_val (V_lit l) ) b1 ∧
                     eval_c i c'[z'::=V_var z2]_v[z2::=V_var x]_v b2" proof -

        have "wfC P B ?G (CE_val v == CE_val (V_lit l))"  using wbc wfC_elims(7) assms subst_cv.simps subst_v_c_def by fastforce

        moreover have "wfC P B ?G (c'[z'::=V_var z2]_v[z2::=V_var x]_v)" proof(rule wfT_wfC_cons)
          show ‹ P; B; Γ ⊨_wf { z1 : b | CE_val v == CE_val (V_lit l) IMP (c[z::=V_var z1]_v) } › using assms subst_v_c_def by auto
          have " { z2 : b | c'[z'::=V_var z2]_v } = { z' : b | c' }" using assms subst_v_c_def by auto
          thus  ‹ P; B; Γ ⊨_wf { z2 : b | c'[z'::=V_var z2]_v } › using assms subtype_elims by metis
          show ‹atom x ♯ (CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v , c'[z'::=V_var z2]_v, Γ)› using xx fresh_Pair c.fresh by metis
        qed

        ultimately show ?thesis using wfI_wfC_eval_c a1 subst_v_c_def by simp
      qed

      ultimately show "is_satis i ?c" using is_satis_imp[OF *] by auto
    qed
    ultimately show  ?thesis using valid.simps by simp
  qed
  moreover have "atom x ♯ (P, B, Γ, z1 , CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v , z2 , CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v )" 
    unfolding fresh_prod5 τ.fresh using xx xf2 fresh_prodN x_fresh_b by metis
  ultimately show ?thesis using subtype_baseI assms  xf2 by metis 
qed

lemma eval_e_concat_eq:
  assumes  "wfI Θ Γ i" 
  shows "∃s. eval_e i (CE_val (V_lit (L_bitvec (v1 @ v2))) ) s ∧ eval_e i (CE_concat [(V_lit (L_bitvec v1))]^ce [(V_lit (L_bitvec v2))]^ce) s"
  using eval_e_valI eval_e_concatI eval_v_litI eval_l.simps by metis

lemma is_satis_eval_e_eq_imp:
  assumes "wfI Θ Γ i" and "eval_e i e1 s" and "eval_e i e2 s"
    and  "is_satis i (CE_val (V_var x) == e1)"  (is "is_satis i ?c1")
  shows "is_satis i (CE_val (V_var x) == e2)"
proof -
  have *:"eval_c i ?c1 True" using assms is_satis.simps by blast
  hence "eval_e i (CE_val (V_var x)) s" using assms is_satis.simps eval_c_elims
    by (metis (full_types) eval_e_uniqueness)
  thus ?thesis using is_satis.simps eval_c.intros assms by fastforce
qed

lemma valid_eval_e_eq:
  fixes e1::ce and e2::ce
  assumes "∀Γ i. wfI Θ Γ i ⟶ (∃s. eval_e i e1 s ∧ eval_e i e2 s)" and "Θ; B; GNil ⊨_wf e1 : b " and  "Θ; B; GNil ⊨_wf e2 : b"
  shows    "Θ; B; (x, b, (CE_val (V_var x) == e1 )) #_\<Gamma> GNil ⊨ (CE_val (V_var x) == e2) "
proof(rule validI)
  show "Θ; B; (x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil ⊨_wf CE_val (V_var x) == e2" 
  proof
    have " Θ ; B ; (x, b, TRUE )#_\<Gamma>GNil ⊨_wf CE_val (V_var x) == e1" using assms wfC_eqI wfE_valI wfV_varI wfX_wfY 
      by (simp add: fresh_GNil wfC_e_eq)    
    hence "Θ ; B ⊨_wf (x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil" using wfG_consI fresh_GNil wfX_wfY assms wfX_wfB by metis
    thus "Θ; B; (x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil ⊨_wf CE_val (V_var x) : b " using  wfCE_valI wfV_varI wfX_wfY 
        lookup.simps  assms wfX_wfY by simp
    show "Θ; B; (x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil ⊨_wf e2 : b " using assms wf_weakening wfX_wfY 
      by (metis (full_types) ‹Θ; B; (x, b, CE_val (V_var x) == e1 ) #_\Γ GNil ⊨_wf CE_val (V_var x) : b› empty_iff subsetI toSet.simps(1))
  qed
  show " ∀i. wfI Θ ((x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil) i ∧ is_satis_g i ((x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil) ⟶ is_satis i (CE_val (V_var x) == e2 )"
  proof(rule,rule)
    fix i
    assume "wfI Θ ((x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil) i ∧ is_satis_g i ((x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil)"
    moreover then obtain s where "eval_e i e1 s ∧ eval_e i e2 s" using assms by auto
    ultimately show "is_satis i (CE_val (V_var x) == e2 )" using assms  is_satis_eval_e_eq_imp is_satis_g.simps by meson
  qed
qed

lemma subtype_concat:
  assumes " ⊨_wf Θ"
  shows "Θ; B; GNil ⊨ { z : B_bitvec | CE_val (V_var z) == CE_val (V_lit (L_bitvec (v1 @ v2))) } <
            { z : B_bitvec | CE_val (V_var z) == CE_concat [(V_lit (L_bitvec v1))]^ce [(V_lit (L_bitvec v2))]^ce }" (is "Θ; B; GNil ⊨ ?t1 < ?t2")
proof -
  obtain x::x where x: "atom x ♯ (Θ, B, GNil, z , CE_val (V_var z) == CE_val (V_lit (L_bitvec (v1 @ v2))),
            z , CE_val (V_var z) == CE_concat [V_lit (L_bitvec v1)]^ce [V_lit (L_bitvec v2)]^ce )" 
    (is "?xfree" )
    using obtain_fresh by auto

  have wb1: "Θ; B; GNil ⊨_wf CE_val (V_lit (L_bitvec (v1 @ v2))) : B_bitvec" using wfX_wfY wfCE_valI wfV_litI assms base_for_lit.simps wfG_nilI by metis
  hence wb2: "Θ; B; GNil ⊨_wf CE_concat [(V_lit (L_bitvec v1))]^ce [(V_lit (L_bitvec v2))]^ce : B_bitvec" 
    using wfCE_concatI wfX_wfY wfV_litI base_for_lit.simps wfCE_valI by metis

  show ?thesis proof
    show " Θ; B; GNil ⊨_wf ?t1" using wfT_e_eq fresh_GNil wb1 wb2 by metis
    show " Θ; B; GNil ⊨_wf ?t2" using wfT_e_eq fresh_GNil wb1 wb2 by metis
    show ?xfree using x by auto
    show "Θ; B; (x, B_bitvec, (CE_val (V_var z) == CE_val (V_lit (L_bitvec (v1 @ v2))) )[z::=V_var x]_v) #_\<Gamma>
           GNil ⊨ (CE_val (V_var z) == CE_concat [(V_lit (L_bitvec v1))]^ce [(V_lit (L_bitvec v2))]^ce )[z::=V_var x]_v " 
      using valid_eval_e_eq eval_e_concat_eq wb1 wb2 subst_v_c_def by fastforce
  qed
qed

lemma subtype_len:
  assumes " ⊨_wf Θ"
  shows "Θ; B; 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 }" (is "Θ; B; GNil ⊨ ?t1 < ?t2")
proof -

  have *: "Θ ⊨_wf [] ∧ Θ; B; GNil ⊨_wf []_\<Delta> " using assms wfG_nilI wfD_emptyI wfPhi_emptyI by auto
  obtain x::x where x: "atom x ♯ (Θ, B, GNil, z' , CE_val (V_var z') ==
          CE_val (V_lit (L_num (int (length v)))) , z, CE_val (V_var z) == CE_len [(V_lit (L_bitvec v))]^ce )"
    (is "atom x ♯ ?F")
    using obtain_fresh by metis
  then show ?thesis proof
    have "Θ ; B ; GNil ⊨_wf CE_val (V_lit (L_num (int (length v)))) : B_int" 
      using wfCE_valI * wfV_litI base_for_lit.simps 
      by (metis wfE_valI wfX_wfY)

    thus  "Θ; B; GNil ⊨_wf ?t1" using wfT_e_eq fresh_GNil by auto

    have "Θ ; B ; GNil ⊨_wf CE_len [(V_lit (L_bitvec v))]^ce : B_int"       
      using wfE_valI * wfV_litI base_for_lit.simps  wfE_valI wfX_wfY 
      by (metis wfCE_lenI wfCE_valI)

    thus "Θ; B; GNil ⊨_wf ?t2" using wfT_e_eq fresh_GNil  by auto

    show  "Θ; B; (x, B_int, (CE_val (V_var z') == CE_val (V_lit (L_num (int (length v)))) )[z'::=V_var x]_v) #_\<Gamma> GNil ⊨ (CE_val (V_var z) == CE_len [(V_lit (L_bitvec v))]^ce )[z::=V_var x]_v"
      (is "Θ; B; ?G ⊨ ?c" ) using valid_len assms subst_v_c_def by auto      
  qed
qed

lemma subtype_base_fresh:
  assumes "Θ; B; Γ ⊨_wf { z : b | c }" and "Θ; B; Γ ⊨_wf { z : b | c' } " and
    "atom z ♯ Γ" and "Θ; B; (z, b, c) #_\<Gamma> Γ ⊨ c'"
  shows "Θ; B; Γ ⊨ { z : b | c } < { z : b | c' }"
proof  -
  obtain x::x where *:"atom x ♯ ((Θ , B , z, c, z, c', Γ) , (Θ, B, Γ, { z : b | c }, { z : b | c' }))" using obtain_fresh by metis
  moreover hence "atom x ♯ Γ" using fresh_Pair by auto
  moreover hence "Θ; B; (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ ⊨ c'[z::=V_var x]_v" using assms valid_flip_simple  * subst_v_c_def  by auto
  ultimately show ?thesis using subtype_baseI assms τ.fresh fresh_Pair by metis
qed

lemma subtype_bop_arith:
  assumes "wfG Θ B Γ" and "(opp = Plus ∧ ll = (L_num (n1+n2))) ∨ (opp = LEq ∧ ll = ( if n1≤n2 then L_true else L_false))"  
    and "(opp = Plus ⟶ b = B_int) ∧ (opp = LEq ⟶ b = B_bool)"
  shows "Θ; B; Γ ⊨ ({ z : b | C_eq (CE_val (V_var z)) (CE_val (V_lit (ll))) }) <
                           { z : b | C_eq (CE_val (V_var z)) (CE_op opp [(V_lit (L_num n1))]^ce [(V_lit (L_num n2))]^ce) }" (is "Θ; B; Γ ⊨ ?T1 < ?T2")   
proof -  
  obtain x::x where  xf: "atom x ♯ (z, CE_val (V_var z) == CE_val (V_lit (ll)) , z, CE_val (V_var z) == CE_op opp [(V_lit (L_num n1))]^ce [(V_lit (L_num n2))]^ce , Γ)" 
    using obtain_fresh by blast

  have "Θ; B; Γ ⊨ ({ x : b | C_eq (CE_val (V_var x)) (CE_val (V_lit (ll))) }) <
                           { x : b | C_eq (CE_val (V_var x)) (CE_op opp [(V_lit (L_num n1))]^ce [(V_lit (L_num n2))]^ce) }" (is "Θ; B; Γ ⊨ ?S1 < ?S2") 
  proof(rule  subtype_base_fresh)

    show "atom x ♯ Γ" using xf fresh_Pair by auto

    show  "wfT Θ B Γ ({ x : b | CE_val (V_var x) == CE_val (V_lit ll) })" (is "wfT Θ B ?A ?B") 
    proof(rule wfT_e_eq)
      have   " Θ; B; Γ ⊨_wf (V_lit ll) : b" using wfV_litI base_for_lit.simps assms by metis
      thus " Θ; B; Γ ⊨_wf CE_val (V_lit ll) : b" using wfCE_valI by auto
      show "atom x ♯ Γ" using xf fresh_Pair by auto
    qed

    consider "opp = Plus" | "opp = LEq" using opp.exhaust assms by blast
    then show  "wfT Θ B Γ ({ x : b | CE_val (V_var x) == CE_op opp [(V_lit (L_num n1))]^ce [(V_lit (L_num n2))]^ce })" (is "wfT Θ B ?A ?C")
    proof(cases)
      case 1
      then show "Θ ; B ; Γ ⊨_wf { x : b | [ [ x ]^v ]^ce == [ opp [ [ L_num n1 ]^v ]^ce [ [ L_num n2 ]^v ]^ce ]^ce }"   
        using wfCE_valI  wfCE_plusI  assms wfV_litI base_for_lit.simps assms 
        by (metis ‹atom x ♯ Γ› wfT_e_eq)
    next
      case 2
      then show "Θ ; B ; Γ ⊨_wf { x : b | [ [ x ]^v ]^ce == [ opp [ [ L_num n1 ]^v ]^ce [ [ L_num n2 ]^v ]^ce ]^ce } "  
        using wfCE_valI  wfCE_plusI  assms wfV_litI base_for_lit.simps assms 

        by (metis ‹atom x ♯ Γ› wfCE_leqI wfT_e_eq)
    qed    

    show   "Θ; B ; (x, b, (CE_val (V_var x) == CE_val (V_lit (ll)) )) #_\<Gamma> Γ
                          ⊨ (CE_val (V_var x) == CE_op opp [V_lit (L_num n1)]^ce [V_lit (L_num n2)]^ce)" (is "Θ; B; ?G ⊨ ?c")
      using valid_arith_bop assms xf by simp

  qed
  moreover have "?S1 = ?T1 " using type_l_eq by auto
  moreover have "?S2 = ?T2" using type_e_eq ce.fresh v.fresh supp_l_empty fresh_def empty_iff fresh_e_opp 
    by (metis ms_fresh_all(4))
  ultimately show ?thesis by auto 

qed

lemma subtype_bop_eq:
  assumes "wfG Θ B Γ" and "base_for_lit l1 = base_for_lit l2"
  shows "Θ; B; Γ ⊨ ({ z : B_bool | C_eq (CE_val (V_var z)) (CE_val (V_lit (if l1 = l2 then L_true else L_false))) }) <
                      { z : B_bool | C_eq (CE_val (V_var z)) (CE_op Eq [(V_lit l1)]^ce [(V_lit l2)]^ce) }" (is "Θ; B; Γ ⊨ ?T1 < ?T2")   
proof -
  let ?ll = "if l1 = l2 then L_true else L_false"
  obtain x::x where  xf: "atom x ♯ (z, CE_val (V_var z) == CE_val (V_lit (if l1 = l2 then L_true else L_false)) , z, CE_val (V_var z) == CE_op Eq [(V_lit l1)]^ce [(V_lit l2)]^ce , Γ, (Θ, B, Γ))" 
    using obtain_fresh by blast

  have "Θ; B; Γ ⊨ ({ x : B_bool | C_eq (CE_val (V_var x)) (CE_val (V_lit (?ll))) }) <
                           { x : B_bool | C_eq (CE_val (V_var x)) (CE_op Eq [(V_lit (l1))]^ce [(V_lit (l2))]^ce) }" (is "Θ; B; Γ ⊨ ?S1 < ?S2") 
  proof(rule  subtype_base_fresh)

    show "atom x ♯ Γ" using xf fresh_Pair by auto

    show  "wfT Θ B Γ ({ x : B_bool | CE_val (V_var x) == CE_val (V_lit ?ll) })" (is "wfT Θ B ?A ?B") 
    proof(rule wfT_e_eq)
      have   " Θ; B; Γ ⊨_wf (V_lit ?ll) : B_bool" using wfV_litI base_for_lit.simps assms by metis
      thus " Θ; B; Γ ⊨_wf CE_val (V_lit ?ll) : B_bool" using wfCE_valI by auto
      show "atom x ♯ Γ" using xf fresh_Pair by auto
    qed

    show " Θ ; B ; Γ ⊨_wf { x : B_bool | [ [ x ]^v ]^ce == [ eq [ [ l1 ]^v ]^ce [ [ l2 ]^v ]^ce ]^ce } "   
    proof(rule wfT_e_eq)
      show "Θ ; B ; Γ ⊨_wf [ eq [ [ l1 ]^v ]^ce [ [ l2 ]^v ]^ce ]^ce : B_bool" 
        apply(rule wfCE_eqI, rule wfCE_valI)
        apply(rule wfV_litI, simp add: assms)
        using wfV_litI assms wfCE_valI by auto   
      show "atom x ♯ Γ"  using xf fresh_Pair by auto
    qed

    show   "Θ; B ; (x, B_bool, (CE_val (V_var x) == CE_val (V_lit (?ll)) )) #_\<Gamma> Γ
                          ⊨ (CE_val (V_var x) == CE_op Eq [V_lit (l1)]^ce [V_lit (l2)]^ce)" (is "Θ; B; ?G ⊨ ?c")
      using valid_eq_bop assms xf by auto

  qed
  moreover have "?S1 = ?T1 " using type_l_eq by auto
  moreover have "?S2 = ?T2" using type_e_eq ce.fresh v.fresh supp_l_empty fresh_def empty_iff fresh_e_opp 
    by (metis ms_fresh_all(4))
  ultimately show ?thesis by auto 

qed

lemma subtype_top:
  assumes "wfT Θ B G ({ z : b | c })"
  shows  "Θ; B; G ⊨ ({ z : b | c }) < ({ z : b | TRUE })"
proof - 
  obtain x::x where *: "atom x ♯ (Θ, B, G, z , c, z , TRUE)" using obtain_fresh by blast
  then show ?thesis proof(rule subtype_baseI)
    show ‹ Θ; B; G ⊨_wf { z : b | c } › using assms by auto
    show ‹ Θ; B;G ⊨_wf { z : b | TRUE } › using wfT_TRUE assms wfX_wfY b_of.simps wfT_wf
      by (metis wfX_wfB(8))
    hence "Θ ; B ⊨_wf (x, b, c[z::=V_var x]_v) #_\<Gamma> G" using wfT_wf_cons3 assms fresh_Pair * subst_v_c_def by auto
    thus  ‹Θ; B; (x, b, c[z::=V_var x]_v) #_\Γ G ⊨ (TRUE)[z::=V_var x]_v › using valid_trueI subst_cv.simps subst_v_c_def by metis
  qed
qed

lemma if_simp:
  "(if x = x then e1 else e2) = e1"
  by auto

lemma subtype_split:
  assumes "split n v (v1,v2)" and "⊨_wf Θ"
  shows "Θ ; {||} ; GNil ⊨ { z : [ B_bitvec , B_bitvec ]^b | [ [ z ]^v ]^ce == [ [ [ L_bitvec
           v1 ]^v , [ L_bitvec
                       v2 ]^v ]^v ]^ce } < { z : [ B_bitvec , B_bitvec ]^b | [ [ L_bitvec
          v ]^v ]^ce == [ [#1[ [ z ]^v ]^ce]^ce @@ [#2[ [ z ]^v ]^ce]^ce ]^ce AND [| [#1[ [ z ]^v ]^ce]^ce |]^ce == [ [ L_num
                                                             n ]^v ]^ce }" 
    (is "Θ ;?B ; GNil ⊨ { z : [ B_bitvec , B_bitvec ]^b | ?c1 } < { z : [ B_bitvec , B_bitvec ]^b | ?c2 }")
proof -
  obtain x::x where xf:"atom x ♯ (Θ, ?B, GNil, z, ?c1,z, ?c2 )"  using obtain_fresh by auto
  then show ?thesis proof(rule subtype_baseI)
    show *: ‹Θ ; ?B ; (x, [ B_bitvec , B_bitvec ]^b, (?c1)[z::=[ x ]^v]_v) #_\Γ
 GNil ⊨ (?c2)[z::=[ x ]^v]_v ›
      unfolding subst_v_c_def subst_cv.simps subst_cev.simps subst_vv.simps if_simp      
      using valid_split[OF assms, of x] by simp
    show ‹ Θ ; ?B ; GNil ⊨_wf { z : [ B_bitvec , B_bitvec ]^b| ?c1 } › using valid_wfT[OF *] xf fresh_prodN by metis
    show ‹ Θ ; ?B ; GNil ⊨_wf { z : [ B_bitvec , B_bitvec ]^b| ?c2 } ›  using valid_wfT[OF *] xf fresh_prodN by metis
  qed
qed

lemma subtype_range:
  fixes n::int and Γ::Γ
  assumes "0 ≤ n ∧ n ≤ int (length v)" and "Θ ; {||} ⊨_wf Γ" 
  shows "Θ ; {||} ; Γ ⊨ { z : B_int | [ [ z ]^v ]^ce == [ [ L_num n ]^v ]^ce } <
                           { 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) }"
    (is  "Θ ; ?B ; Γ ⊨ { z : B_int | ?c1 } < { z : B_int | ?c2 AND ?c3 }")
proof -
  obtain x::x where *:‹atom x ♯ (Θ, ?B, Γ, z, ?c1 , z, ?c2 AND ?c3)› using obtain_fresh by auto
  moreover have **:‹Θ ; ?B ; (x, B_int, (?c1)[z::=[ x ]^v]_v) #_\Γ Γ ⊨ (?c2 AND ?c3)[z::=[ x ]^v]_v›
    unfolding subst_v_c_def subst_cv.simps subst_cev.simps subst_vv.simps if_simp using valid_range_length[OF assms(1)] assms fresh_prodN * by simp

  moreover hence ‹ Θ ; ?B ; Γ ⊨_wf { z : B_int | [ [ z ]^v ]^ce == [ [ L_num n ]^v ]^ce } › using 
      valid_wfT * fresh_prodN by metis
  moreover have ‹ Θ ; ?B ; Γ ⊨_wf { z : B_int | ?c2 AND ?c3 } ›
    using valid_wfT[OF **]  * fresh_prodN by metis
  ultimately show ?thesis using subtype_baseI by auto
qed

lemma check_num_range:
  assumes "0 ≤ n ∧ n ≤ int (length v)" and "⊨_wf Θ"
  shows "Θ ; {||} ; 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 assms subtype_range check_v.intros infer_v_litI wfG_nilI 
  by (meson infer_natI)

section ‹Literals›

nominal_function type_for_lit :: "l ==> τ" where
  "type_for_lit (L_true) = ({ z : B_bool | [[z]^v]^ce == [V_lit L_true]^ce })"
| "type_for_lit (L_false) = ({ z : B_bool | [[z]^v]^ce == [V_lit L_false]^ce })"
| "type_for_lit (L_num n) = ({ z : B_int | [[z]^v]^ce == [V_lit (L_num n)]^ce })"
| "type_for_lit (L_unit) = ({ z : B_unit | [[z]^v]^ce == [V_lit (L_unit )]^ce })" (* could have done { z : unit | True } but want the uniformity *)
| "type_for_lit (L_bitvec v) = ({ z : B_bitvec | [[z]^v]^ce == [V_lit (L_bitvec v)]^ce })"
  by (auto simp: eqvt_def type_for_lit_graph_aux_def, metis l.strong_exhaust,(simp add: permute_int_def flip_bitvec0)+ )
nominal_termination (eqvt) by lexicographic_order


nominal_function type_for_var :: "Γ ==> τ ==> x ==> τ" where
  "type_for_var G τ x = (case lookup G x of
                       None ==> τ
                  | Some (b,c) ==> ({ x : b | c })) "  
  apply auto  unfolding eqvt_def apply(rule allI)  unfolding type_for_var_graph_aux_def eqvt_def by simp
nominal_termination (eqvt) by lexicographic_order

lemma infer_l_form:
  fixes l::l and tm::"'a::fs"
  assumes "⊨ l ==> τ" 
  shows "∃z b. τ = ({ z : b | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) }) ∧ atom z ♯ tm"
proof -
  obtain z' and b where t:"τ = ({ z' : b | C_eq (CE_val (V_var z')) (CE_val (V_lit l)) })" using infer_l_elims  assms  using infer_l.simps type_for_lit.simps 
      type_for_lit.cases by blast
  obtain z::x where zf: "atom z ♯ tm" using obtain_fresh by metis
  have "τ = { z : b | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) }" using type_e_eq ce.fresh v.fresh l.fresh 
    by (metis t type_l_eq)
  thus ?thesis using zf by auto
qed

lemma infer_l_form3:
  fixes l::l
  assumes "⊨ l ==> τ" 
  shows "∃z. τ = ({ z : base_for_lit l | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) })"
  using infer_l_elims using assms  using infer_l.simps type_for_lit.simps base_for_lit.simps by auto

lemma infer_l_form4[simp]:
  fixes Γ::Γ
  assumes "Θ ; B ⊨_wf Γ "   
  shows "∃z. ⊨ l ==> ({ z : base_for_lit l | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) })"
  using assms  infer_l_form2 infer_l_form3 by metis

lemma infer_v_unit_form:
  fixes v::v
  assumes "P ; B ; Γ ⊨ v ==> ({ z1 : B_unit | c1 })" and "supp v = {}"
  shows "v = V_lit L_unit"
  using assms proof(nominal_induct Γ v "{ z1 : B_unit | c1 }" rule: infer_v.strong_induct)
  case (infer_v_varI Θ B c x z)
  then show ?case using supp_at_base by auto
next
  case (infer_v_litI Θ B Γ l)
  from ‹⊨ l ==> { z1 : B_unit | c1 }›  show ?case by(nominal_induct "{ z1 : B_unit | c1 }" rule: infer_l.strong_induct,auto)
qed

lemma base_for_lit_wf:
  assumes "⊨_wf Θ"
  shows   "Θ ; B ⊨_wf base_for_lit l"
  using base_for_lit.simps using  wfV_elims wf_intros  assms l.exhaust by metis

lemma infer_l_t_wf:
  fixes Γ::Γ
  assumes "Θ ; B ⊨_wf Γ ∧ atom z ♯ Γ"
  shows  "Θ; B; Γ ⊨_wf { z : base_for_lit l | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) }"
proof 
  show "atom z ♯ (Θ, B, Γ)" using  wfG_fresh_x assms by auto
  show "Θ ; B ⊨_wf base_for_lit l" using base_for_lit_wf assms wfX_wfY by metis
  thus "Θ; B; (z, base_for_lit l, TRUE) #_\<Gamma> Γ ⊨_wf CE_val (V_var z) == CE_val (V_lit l)" using wfC_v_eq wfV_litI assms wfX_wfY by metis
qed

lemma infer_l_wf:
  fixes l::l and Γ::Γ and τ::τ and Θ::Θ
  assumes "⊨ l ==> τ" and "Θ ; B ⊨_wf Γ"
  shows "⊨_wf Θ" and  "Θ ; B ⊨_wf Γ" and "Θ; B; Γ ⊨_wf τ"
proof -
  show *:"Θ ; B ⊨_wf Γ" using assms infer_l_elims by auto
  thus  "⊨_wf Θ" using wfX_wfY by auto
  show *:"Θ ; B ; Γ ⊨_wf τ" using infer_l_t_wf assms infer_l_form3 * 
    by (metis ‹⊨_wf Θ› fresh_GNil wfG_nilI wfT_weakening_nil)
qed

lemma infer_l_uniqueness: 
  fixes l::l
  assumes "⊨ l ==> τ" and "⊨ l ==> τ'" 
  shows "τ = τ'"
  using assms
proof -
  obtain z and b where zt: "τ = ({ z : b | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) })" using infer_l_form assms by blast
  obtain z' and b where z't: "τ' = ({ z' : b | C_eq (CE_val (V_var z')) (CE_val (V_lit l)) })" using infer_l_form assms   by blast
  thus ?thesis using type_l_eq zt z't   assms infer_l.simps infer_l_elims l.distinct    
    by (metis infer_l_form3)
qed

section ‹Values›

lemma type_v_eq:
  assumes "{ z1 : b1 | c1 } = { z : b | C_eq (CE_val (V_var z)) (CE_val (V_var x)) }" and "atom z ♯ x"
  shows "b = b1" and "c1 = C_eq (CE_val (V_var z1)) (CE_val (V_var x))"
  using assms  by (auto,metis Abs1_eq_iff τ.eq_iff assms c.fresh ce.fresh type_e_eq v.fresh)

lemma infer_var2 [elim]:
  assumes "P; B ; G ⊨ V_var x ==> τ"
  shows "∃b c. Some (b,c) = lookup G x"
  using assms infer_v_elims lookup_iff   by (metis (no_types, lifting))

lemma infer_var3 [elim]:
  assumes "Θ; B; Γ ⊨ V_var x ==> τ"
  shows "∃z b c. Some (b,c) = lookup Γ x ∧ τ = ({ z : b | C_eq (CE_val (V_var z)) (CE_val (V_var x)) }) ∧ atom z ♯ x ∧ atom z ♯ (Θ, B, Γ)"
  using infer_v_elims(1)[OF assms(1)] by metis

lemma infer_bool_options2:
  fixes v::v
  assumes "Θ; B; Γ ⊨ v ==> { z : b | c }" and "supp v = {} ∧ b = B_bool"
  shows  "v = V_lit L_true ∨ (v = (V_lit L_false))"
  using assms
proof(nominal_induct "{ z : b | c }"  rule: infer_v.strong_induct)
  case (infer_v_varI Θ B Γ c x z)
  then show ?case using v.supp supp_at_base by auto
next
  case (infer_v_litI Θ B Γ l)
  from ‹ ⊨ l ==> { z : b | c }› show ?case proof(nominal_induct "{ z : b | c }"  rule: infer_l.strong_induct)
    case (infer_trueI z)
    then show ?case by auto
  next
    case (infer_falseI z)
    then show ?case by auto
  next
    case (infer_natI n z)
    then show ?case using infer_v_litI by simp
  next
    case (infer_unitI z)
    then show ?case using infer_v_litI by simp
  next
    case (infer_bitvecI bv z)
    then show ?case using infer_v_litI by simp
  qed
qed(auto+)

lemma infer_bool_options:
  fixes v::v
  assumes "Θ; B; Γ ⊨ v ==> { z : B_bool | c }" and "supp v = {}"
  shows "v = V_lit L_true ∨ (v = (V_lit L_false))"
  using infer_bool_options2  assms by blast

lemma infer_int2:
  fixes v::v
  assumes "Θ; B; Γ ⊨ v ==> { z : b | c }"
  shows "supp v = {} ∧ b = B_int ⟶ (∃n. v = V_lit (L_num n))"
  using assms
proof(nominal_induct "{ z : b | c }"  rule: infer_v.strong_induct)
  case (infer_v_varI Θ B Γ c x z)
  then show ?case using v.supp supp_at_base by auto
next
  case (infer_v_litI Θ B Γ l)
  from ‹ ⊨ l ==> { z : b | c }› show ?case proof(nominal_induct "{ z : b | c }"  rule: infer_l.strong_induct)
    case (infer_trueI z)
    then show ?case by auto
  next
    case (infer_falseI z)
    then show ?case by auto
  next
    case (infer_natI n z)
    then show ?case using infer_v_litI by simp
  next
    case (infer_unitI z)
    then show ?case using infer_v_litI by simp
  next
    case (infer_bitvecI bv z)
    then show ?case using infer_v_litI by simp
  qed
qed(auto+)

lemma infer_bitvec:
  fixes Θ::Θ and v::v
  assumes "Θ; B; Γ ⊨ v ==> { z' : B_bitvec | c' }" and "supp v = {}"
  shows "∃bv. v = V_lit (L_bitvec bv)"
  using assms proof(nominal_induct v rule: v.strong_induct)
  case (V_lit l)
  then show ?case by(nominal_induct l rule: l.strong_induct,force+)
next
  case (V_consp s dc b v)
  then show ?case using  infer_v_elims(7)[OF V_consp(2)] τ.eq_iff by auto
next
  case (V_var x)
  then show ?case using supp_at_base by auto
qed(force+)

lemma infer_int:
  assumes "infer_v Θ B Γ v ({ z : B_int | c })" and "supp v= {}"
  shows "∃n. V_lit (L_num n) = v"
  using assms infer_int2  by (metis (no_types, lifting))

lemma infer_lit:
  assumes "infer_v Θ B Γ v ({ z : b | c })" and "supp v= {}" and "b ∈ { B_bool , B_int , B_unit }"
  shows "∃l. V_lit l = v"
  using assms proof(nominal_induct v rule: v.strong_induct)
  case (V_lit x)
  then show ?case   by (simp add: supp_at_base)
next
  case (V_var x)
  then show ?case 
    by (simp add: supp_at_base)
next
  case (V_pair x1a x2a)
  then show ?case  using supp_at_base by auto
next
  case (V_cons x1a x2a x3)
  then show ?case   using supp_at_base by auto
next
  case (V_consp x1a x2a x3 x4)
  then show ?case    using supp_at_base by auto
qed

lemma infer_v_form[simp]:
  fixes v::v
  assumes "Θ; B; Γ ⊨ v ==> τ" 
  shows "∃z b. τ = ({ z : b | C_eq (CE_val (V_var z)) (CE_val v)}) ∧ atom z ♯ v ∧ atom z ♯ (Θ, B, Γ)"
  using assms
proof(nominal_induct   rule: infer_v.strong_induct)
  case (infer_v_varI Θ B Γ b c x z)
  then show ?case by force
next
  case (infer_v_litI Θ B Γ l τ)
  then obtain z and b where "τ = { z : b | CE_val (V_var z) == CE_val (V_lit l) } ∧atom z ♯ (Θ, B, Γ) "
    using infer_l_form by metis
  moreover hence  "atom z ♯ (V_lit l)" using supp_l_empty v.fresh(1) fresh_prod2 fresh_def by blast
  ultimately show ?case by metis
next
  case (infer_v_pairI z v1 v2 Θ B Γ t1 t2)
  then show ?case by force
next
  case (infer_v_consI s dclist Θ dc tc B Γ v tv z)
  moreover hence "atom z ♯ (V_cons s dc v)" using
      Un_commute b.supp(3) fresh_def sup_bot.right_neutral supp_b_empty v.supp(4) pure_supp by metis
  ultimately show ?case using fresh_prodN by metis
next
  case (infer_v_conspI s bv dclist Θ dc tc B Γ v tv b z)
  moreover hence "atom z ♯ (V_consp s dc b v)" unfolding v.fresh using pure_fresh fresh_prodN * by metis
  ultimately show ?case using fresh_prodN by metis
qed

lemma infer_v_form2:
  fixes v::v
  assumes "Θ; B; Γ ⊨ v ==> ({ z : b | c })" and "atom z ♯ v" 
  shows "c = C_eq (CE_val (V_var z)) (CE_val v)"
  using assms 
proof -
  obtain z' and b' where "({ z : b | c }) = ({ z' : b' | CE_val (V_var z') == CE_val v }) ∧ atom z' ♯ v"
    using infer_v_form assms by meson
  thus ?thesis using Abs1_eq_iff(3) τ.eq_iff  type_e_eq
    by (metis assms(2) ce.fresh(1))
qed

lemma infer_v_form3:
  fixes v::v
  assumes "Θ; B; Γ ⊨ v ==> τ"  and "atom z ♯ (v,Γ)"
  shows "Θ; B; Γ ⊨ v ==> { z : b_of τ | C_eq (CE_val (V_var z)) (CE_val v)}"
proof -
  obtain z' and b' where "τ = { z' : b' | C_eq (CE_val (V_var z')) (CE_val v)} ∧ atom z' ♯ v ∧ atom z' ♯ (Θ, B, Γ)" 
    using infer_v_form assms by metis
  moreover hence "{ z' : b' | C_eq (CE_val (V_var z')) (CE_val v)} = { z : b' | C_eq (CE_val (V_var z)) (CE_val v)}" 
    using assms type_e_eq fresh_Pair ce.fresh by auto
  ultimately show  ?thesis using  b_of.simps assms by auto
qed

lemma infer_v_form4:
  fixes v::v
  assumes "Θ; B; Γ ⊨ v ==> τ"  and "atom z ♯ (v,Γ)" and "b = b_of τ"
  shows "Θ; B; Γ ⊨ v ==> { z : b | C_eq (CE_val (V_var z)) (CE_val v)}"
  using assms infer_v_form3 by simp

lemma infer_v_v_wf:
  fixes v::v
  shows "Θ; B ; G ⊨ v ==> τ ==> Θ; B; G ⊨_wf v : (b_of τ)"
proof(induct rule: infer_v.induct)
  case (infer_v_varI Θ B Γ b c x z)
  then show ?case using  wfC_elims  wf_intros by auto
next
  case (infer_v_pairI z v1 v2 Θ B Γ t1 t2)
  then show ?case using  wfC_elims  wf_intros by auto
next
  case (infer_v_litI Θ B Γ l τ)
  hence "b_of τ = base_for_lit l" using infer_l_form3 b_of.simps by metis
  then show ?case using wfV_litI infer_l_wf infer_v_litI wfG_b_weakening
    by (metis fempty_fsubsetI)
next
  case (infer_v_consI s dclist Θ dc tc B Γ v tv z)
  then show ?case using  wfC_elims  wf_intros 
    by (metis (no_types, lifting) b_of.simps has_fresh_z2 subtype_eq_base2)
next
  case (infer_v_conspI s bv dclist Θ dc tc B Γ v tv b z)
  obtain z1 b1 c1 where t:"tc = { z1 : b1 | c1 }" using obtain_fresh_z by metis
  show ?case unfolding b_of.simps proof(rule wfV_conspI)
    show ‹AF_typedef_poly s bv dclist ∈ set Θ› using infer_v_conspI by auto
    show ‹(dc, { z1 : b1 | c1 } ) ∈ set dclist› using infer_v_conspI t by auto
    show ‹ Θ ; B ⊨_wf b › using infer_v_conspI by auto
    show ‹atom bv ♯ (Θ, B, Γ, b, v)› using infer_v_conspI by auto
    have " b1[bv::=b]_bb = b_of tv" using subtype_eq_base2[OF infer_v_conspI(5)] b_of.simps t subst_tb.simps by auto
    thus ‹ Θ; B; Γ ⊨_wf v : b1[bv::=b]_bb › using infer_v_conspI by auto
  qed
qed

lemma infer_v_t_form_wf:
  assumes " wfB Θ B b" and "wfV Θ B Γ v b" and "atom z ♯ Γ"
  shows "wfT Θ B Γ { z : b | C_eq (CE_val (V_var z)) (CE_val v)}"
  using wfT_v_eq assms by auto

lemma infer_v_t_wf:
  fixes v::v
  assumes "Θ; B; G ⊨ v ==> τ"
  shows "wfT Θ B G τ ∧ wfB Θ B (b_of τ) "
proof -
  obtain z and b where "τ = { z : b | CE_val (V_var z) == CE_val v } ∧ atom z ♯ v ∧ atom z ♯ (Θ, B, G)" using infer_v_form assms by metis
  moreover have  "wfB Θ B b" using infer_v_v_wf b_of.simps wfX_wfB(1) assms 
    using calculation by fastforce
  ultimately show "wfT Θ B G τ ∧ wfB Θ B (b_of τ)" using infer_v_v_wf  infer_v_t_form_wf assms by fastforce
qed

lemma infer_v_wf: 
  fixes  v::v
  assumes "Θ; B; G ⊨ v ==> τ"
  shows  "Θ; B; G ⊨_wf v : (b_of τ)" and "wfT Θ B G τ"  and "wfTh Θ" and "wfG Θ B G"
proof -
  show "Θ; B; G ⊨_wf v : b_of τ " using infer_v_v_wf assms by auto
  show "Θ; B; G ⊨_wf τ" using infer_v_t_wf assms by auto
  thus  "Θ ; B ⊨_wf G" using wfX_wfY by auto
  thus  "⊨_wf Θ" using  wfX_wfY by auto
qed

lemma check_bool_options:
  assumes "Θ; B; Γ ⊨ v <== { z : B_bool | TRUE }" and "supp v = {}"
  shows "v = V_lit L_true ∨ v = V_lit L_false"
proof -
  obtain t1 where  " Θ; B; Γ ⊨ t1 < { z : B_bool | TRUE } ∧ Θ; B; Γ ⊨ v ==> t1" using check_v_elims 
    using assms by blast
  thus ?thesis using infer_bool_options assms
    by (metis τ.exhaust b_of.simps subtype_eq_base2)
qed

lemma check_v_wf:
  fixes v::v and Γ::Γ and τ::τ
  assumes "Θ; B; Γ ⊨ v <== τ"
  shows " Θ ; B ⊨_wf Γ" and "Θ; B;Γ ⊨_wf v : b_of τ" and "Θ; B;Γ ⊨_wf τ"
proof -
  obtain τ' where *: "Θ; B; Γ ⊨ τ' < τ ∧ Θ; B; Γ ⊨ v ==> τ'" using check_v_elims assms by auto
  thus "Θ ; B ⊨_wf Γ " and "Θ; B;Γ ⊨_wf v : b_of τ" and "Θ; B; Γ ⊨_wf τ"  
    using infer_v_wf infer_v_v_wf  subtype_eq_base2   *  subtype_wf  by metis+
qed

lemma infer_v_form_fresh:
  fixes v::v and t::"'a::fs" 
  assumes "Θ; B; Γ ⊨ v ==> τ" 
  shows "∃z b. τ = { z : b | C_eq (CE_val (V_var z)) (CE_val v)} ∧ atom z ♯ (t,v)"
proof -
  obtain z' and b' where "τ = { z' : b' | C_eq (CE_val (V_var z')) (CE_val v)}" using infer_v_form assms by blast
  moreover then obtain z and b and c where "τ = { z : b | c } ∧ atom z ♯ (t,v)" using obtain_fresh_z by metis
  ultimately have "τ = { z : b | C_eq (CE_val (V_var z)) (CE_val v)} ∧ atom z ♯ (t,v) "
    using assms infer_v_form2  by auto
  thus ?thesis by blast
qed

text ‹ More generally, if support of a term is empty then any G will do ›

lemma infer_v_form_consp:
  assumes "Θ; B; Γ ⊨ V_consp s dc b v ==> τ"
  shows "b_of τ = B_app s b"
  using assms proof(nominal_induct "V_consp s dc b v" τ   rule: infer_v.strong_induct)
  case (infer_v_conspI bv dclist Θ tc B Γ tv z)
  then show ?case using b_of.simps by metis
qed

lemma lookup_in_rig_b:
  assumes "Some (b2, c2) = lookup (Γ[x⟼c']) x'" and
    "Some (b1, c1) = lookup Γ x'"
  shows "b1 = b2"
  using assms lookup_in_rig[OF assms(2)] 
  by (metis option.inject prod.inject)

lemma infer_v_uniqueness_rig:
  fixes x::x and c::c
  assumes "infer_v P B G v τ" and "infer_v P B (replace_in_g G x c') v τ'"
  shows "τ = τ'"
  using assms
proof(nominal_induct "v"  arbitrary: τ' τ rule: v.strong_induct)
  case (V_lit l)
  hence "infer_l l τ" and "infer_l l τ'" using assms(1) infer_v_elims(2) by auto
  then show ?case using infer_l_uniqueness  by presburger
next
  case (V_var y)

  obtain b and c where bc: "Some (b,c) = lookup G y"  
    using assms(1) infer_v_elims(2)  using V_var.prems(1) lookup_iff by force
  then obtain  c'' where bc':"Some (b,c'') = lookup (replace_in_g G x c') y" 
    using lookup_in_rig by blast

  obtain z  where "τ = ({ z : b | C_eq (CE_val (V_var z)) (CE_val (V_var y)) })" using infer_v_elims(1)[of P B G y τ] V_var
      bc option.inject prod.inject lookup_in_g by metis
  moreover obtain z' where "τ' = ({ z' : b | C_eq (CE_val (V_var z')) (CE_val (V_var y)) })" using infer_v_elims(1)[of P B _ y τ']  V_var
      option.inject prod.inject  lookup_in_rig  by (metis bc')
  ultimately show ?case using type_e_eq 
    by (metis V_var.prems(1) V_var.prems(2) τ.eq_iff ce.fresh(1) finite.emptyI fresh_atom_at_base 
        fresh_finite_insert infer_v_elims(1) v.fresh(2))
next 
  case (V_pair v1 v2)
  obtain  z and z1 and z2 and t1 and t2 and c1 and c2 where
    t1: "τ = ({ z : [ b_of t1 , b_of t2 ]^b | CE_val (V_var z) == CE_val (V_pair v1 v2) }) ∧
           atom z ♯ (v1, v2) ∧ P ; B ; G ⊨ v1 ==> t1 ∧ P ; B ; G ⊨ v2 ==> t2"
    using infer_v_elims(3)[OF V_pair(3)] by metis
  moreover obtain  z' and z1' and z2' and t1' and t2' and c1' and c2' where
    t2: "τ' = ({ z' : [ b_of t1' , b_of t2' ]^b | CE_val (V_var z') == CE_val (V_pair v1 v2) }) ∧
             atom z' ♯ (v1, v2) ∧ P ; B ; (replace_in_g G x c') ⊨ v1 ==> t1' ∧
             P ; B ; (replace_in_g G x c') ⊨ v2 ==> t2'"
    using infer_v_elims(3)[OF V_pair(4)] by metis
  ultimately have "t1 = t1' ∧ t2 = t2'" using V_pair.hyps(1) V_pair.hyps(2) τ.eq_iff by blast
  then show ?case using t1 t2 by simp
next
  case (V_cons s dc v)
  obtain x and z and tc and dclist where  t1: "τ = ({ z : B_id s | CE_val (V_var z) == CE_val (V_cons s dc v) }) ∧
          AF_typedef s dclist ∈ set P ∧
        (dc, tc) ∈ set dclist ∧ atom z ♯ v" 
    using infer_v_elims(4)[OF V_cons(2)] by metis
  moreover obtain x' and z' and tc' and dclist' where  t2: "τ' = ({ z' : B_id s | CE_val (V_var z') == CE_val (V_cons s dc v) })
  ∧ AF_typedef s dclist' ∈ set P ∧ (dc, tc') ∈ set dclist' ∧ atom z' ♯ v" 
    using infer_v_elims(4)[OF V_cons(3)] by metis
  moreover have a: "AF_typedef s dclist' ∈ set P" and b:"(dc,tc') ∈ set dclist'" and c:"AF_typedef s dclist ∈ set P" and
    d:"(dc, tc) ∈ set dclist" using t1 t2 by auto
  ultimately have "tc = tc'" using wfTh_dc_t_unique2   infer_v_wf(3)[OF V_cons(2)] by metis

  moreover have "atom z ♯ CE_val (V_cons s dc v) ∧ atom z' ♯ CE_val (V_cons s dc v)" 
    using e.fresh(1)  v.fresh(4) t1 t2 pure_fresh by auto
  ultimately have "({ z : B_id s | CE_val (V_var z) == CE_val (V_cons s dc v) }) = ({ z' : B_id s | CE_val (V_var z') == CE_val (V_cons s dc v) })" 
    using type_e_eq by metis
  thus ?case using t1 t2 by simp
next
  case (V_consp s dc b v)
  from V_consp(2) V_consp show ?case proof(nominal_induct  "V_consp s dc b v" τ arbitrary: v rule:infer_v.strong_induct)

    case (infer_v_conspI bv dclist Θ tc B Γ v tv z)

    obtain z3 and b3 where *:"τ' = { z3 : b3 | [ [ z3 ]^v ]^ce == [ V_consp s dc b v ]^ce } ∧ atom z3 ♯ V_consp s dc b v"
      using infer_v_form[OF ‹Θ; B; Γ[x⟼c'] ⊨ V_consp s dc b v ==> τ'› ] by metis
    moreover then have "b3 = B_app s b" using  infer_v_form_consp b_of.simps * infer_v_conspI by metis

    moreover have "{ z3 : B_app s b | [ [ z3 ]^v ]^ce == [ V_consp s dc b v ]^ce } = { z : B_app s b | [ [ z ]^v ]^ce == [ V_consp s dc b v ]^ce }"
    proof - 
      have "atom z3 ♯ [V_consp s dc b v]^ce" using * ce.fresh by auto
      moreover have "atom z ♯ [V_consp s dc b v]^ce" using * infer_v_conspI ce.fresh v.fresh pure_fresh by metis
      ultimately show ?thesis  using type_e_eq  infer_v_conspI v.fresh ce.fresh by metis
    qed
    ultimately  show ?case using * by auto
  qed
qed

lemma infer_v_uniqueness: 
  assumes "infer_v P B G v τ" and "infer_v P B G v τ'"
  shows "τ = τ'"
proof - 
  obtain x::x where "atom x ♯ G" using obtain_fresh by metis
  hence "G [ x ⟼ C_true ] = G" using replace_in_g_forget assms infer_v_wf by fast
  thus ?thesis using infer_v_uniqueness_rig assms by metis
qed

lemma infer_v_tid_form:
  fixes v::v
  assumes "Θ ; B ; Γ ⊨ v ==> { z : B_id tid | c }" and  "AF_typedef tid dclist ∈ set Θ" and "supp v = {}"
  shows "∃dc v' t. v = V_cons tid dc v' ∧ (dc , t ) ∈ set dclist"
  using assms proof(nominal_induct  v "{ z : B_id tid | c }" rule: infer_v.strong_induct)
  case (infer_v_varI Θ B c x z)
  then show ?case using v.supp supp_at_base  by auto
next
  case (infer_v_litI Θ B l)
  then show ?case by auto
next
  case (infer_v_consI dclist1 Θ dc tc B Γ v tv z)
  hence "supp v = {}" using v.supp by simp
  then obtain dca and v' where *:"V_cons tid dc v = V_cons tid dca v'" using infer_v_consI by auto
  hence "dca = dc" using v.eq_iff(4)  by auto
  hence  "V_cons tid dc v = V_cons tid dca v' ∧ (dca, tc) ∈ set dclist1" using infer_v_consI * by auto
  moreover have "dclist = dclist1" using wfTh_dclist_unique infer_v_consI wfX_wfY ‹dca=dc›
  proof -
    show ?thesis
      by (meson ‹AF_typedef tid dclist1 ∈ set Θ› ‹Θ; B; Γ ⊨ v ==> tv› infer_v_consI.prems infer_v_wf(4) wfTh_dclist_unique wfX_wfY) 
  qed
  ultimately show ?case by auto
qed

lemma check_v_tid_form:  
  assumes "Θ ; B ; Γ ⊨ v <== { z : B_id tid | TRUE }"  and "AF_typedef tid dclist ∈ set Θ"  and "supp v = {}"
  shows "∃dc v' t. v = V_cons tid dc v' ∧ (dc , t ) ∈ set dclist"
  using assms proof(nominal_induct  v "{ z : B_id tid | TRUE }" rule: check_v.strong_induct)
  case (check_v_subtypeI Θ B Γ τ1 v)
  then obtain z and c where "τ1 = { z : B_id tid | c }" using subtype_eq_base2 b_of.simps 
    by (metis obtain_fresh_z2)
  then show ?case  using infer_v_tid_form check_v_subtypeI by simp
qed

lemma check_v_num_leq:
  fixes n::int and Γ::Γ
  assumes "0 ≤ n ∧ n ≤ int (length v)" and " ⊨_wf Θ " and "Θ ; {||} ⊨_wf Γ"
  shows "Θ ; {||} ; Γ ⊨ [ 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 ) }" 
proof - 
  have "Θ ; {||} ; Γ ⊨ [ L_num n ]^v ==> { z : B_int | [ [ z ]^v ]^ce == [ [ L_num n ]^v ]^ce }" 
    using infer_v_litI infer_natI wfG_nilI assms by auto
  thus ?thesis using subtype_range[OF assms(1) ] assms check_v_subtypeI by metis
qed

lemma check_int:
  assumes "check_v Θ B Γ v ({ z : B_int | c })" and "supp v = {}"
  shows "∃n. V_lit (L_num n) = v"
  using assms infer_int check_v_elims  by (metis b_of.simps infer_v_form subtype_eq_base2)

definition sble :: "Θ ==> Γ ==> bool" where
  "sble Θ Γ = (∃i. i ⊨ Γ ∧ Θ ; Γ ⊨ i)"

lemma check_v_range:
  assumes "Θ ; B ; Γ ⊨ v2 <== { z : B_int | [ leq [ [ L_num 0 ]^v ]^ce [ [ z ]^v ]^ce ]^ce == [ [ L_true ]^v ]^ce AND
            [ leq [ [ z ]^v ]^ce [| [ v1 ]^ce |]^ce ]^ce == [ [ L_true ]^v ]^ce } "
    (is "Θ ; ?B ; Γ ⊨ v2 <== { z : B_int | ?c1 }") 
    and "v1 = V_lit (L_bitvec bv) ∧ v2 = V_lit (L_num n) " and "atom z ♯ Γ" and "sble Θ Γ"
  shows "0 ≤ n ∧ n ≤ int (length bv)"
proof - 
  have  "Θ ; ?B ; Γ ⊨ { z : B_int | [ [ z ]^v ]^ce == [ [ L_num n ]^v ]^ce } < { z : B_int | ?c1 }" 
    using check_v_elims assms 
    by (metis infer_l_uniqueness infer_natI infer_v_elims(2))
  moreover have "atom z ♯ Γ" using fresh_GNil assms by simp
  ultimately have  "Θ ; ?B ; ((z, B_int, [ [ z ]^v ]^ce == [ [ L_num n ]^v ]^ce ) #_\<Gamma> Γ) ⊨ ?c1" 
    using subtype_valid_simple by auto
  thus ?thesis using assms valid_range_length_inv check_v_wf wfX_wfY sble_def by metis
qed

section ‹Expressions›

lemma infer_e_plus[elim]:
  fixes v1::v and v2::v
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ AE_op Plus v1 v2 ==> τ"
  shows "∃z . ({ z : B_int | C_eq (CE_val (V_var z)) (CE_op Plus [v1]^ce [v2]^ce) } = τ)"
  using infer_e_elims assms by metis

lemma infer_e_leq[elim]:
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ AE_op LEq v1 v2 ==> τ"
  shows "∃z . ({ z : B_bool | C_eq (CE_val (V_var z)) (CE_op LEq [v1]^ce [v2]^ce) } = τ)"
  using infer_e_elims assms by metis

lemma infer_e_eq[elim]:
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ AE_op Eq v1 v2 ==> τ"
  shows "∃z . ({ z : B_bool | C_eq (CE_val (V_var z)) (CE_op Eq [v1]^ce [v2]^ce) } = τ)"
  using infer_e_elims(25)[OF assms] by metis

lemma infer_e_e_wf: 
  fixes e::e
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ e ==> τ" 
  shows "Θ ; Φ ; B ; Γ ; Δ ⊨_wf e : b_of τ" 
  using assms proof(nominal_induct τ avoiding: τ rule: infer_e.strong_induct)
  case (infer_e_valI Θ B Γ Δ' Φ v τ)
  then show ?case using  infer_v_v_wf wf_intros by metis
next
  case (infer_e_plusI Θ B Γ Δ' Φ v1 z1 c1 v2 z2 c2 z3)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_leqI Θ B Γ Δ' v1 z1 c1 v2 z2 c2 z3)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_eqI Θ B Γ Δ' v1 z1 c1 v2 z2 c2 z3)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_appI Θ B Γ Δ Φ f x b c τ' s' v τ'')
  have "Θ ; Φ ; B ; Γ ; Δ ⊨_wf AE_app f v : b_of τ' " proof 
    show ‹ Θ ⊨_wf Φ › using infer_e_appI by auto
    show ‹ Θ; B; Γ ⊨_wf Δ › 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 "Θ; B;Γ ⊨_wf v : b" using infer_e_appI check_v_wf b_of.simps by metis
  qed
  moreover have "b_of τ' = b_of (τ'[x::=v]_v)" using subst_tbase_eq subst_v_τ_def by auto
  ultimately show ?case using infer_e_appI subst_v_c_def subst_b_τ_def by auto
next
  case (infer_e_appPI Θ B Γ Δ Φ b' f bv x b c τ'' s' v τ')

  have "Θ ; Φ ; B ; Γ ; Δ ⊨_wf AE_appP f b' v : (b_of τ'')[bv::=b']_b " proof
    show ‹ Θ ⊨_wf Φ › using infer_e_appPI by auto
    show ‹ Θ; B; Γ ⊨_wf Δ › using infer_e_appPI by auto
    show ‹Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c τ'' s'))) = lookup_fun Φ f› using * infer_e_appPI by metis
    show "Θ ; B ⊨_wf b'" using infer_e_appPI by auto
    show "Θ; B;Γ ⊨_wf v : (b[bv::=b']_b)" using infer_e_appPI check_v_wf b_of.simps subst_b_b_def by metis
    have "atom bv ♯ (b_of τ'')[bv::=b']_bb" using fresh_subst_if subst_b_b_def infer_e_appPI by metis
    thus  "atom bv ♯ (Φ, Θ, B, Γ, Δ, b', v, (b_of τ'')[bv::=b']_b)" using infer_e_appPI fresh_prodN subst_b_b_def by metis
  qed
  moreover have "b_of τ' = (b_of τ'')[bv::=b']_b" 
    using ‹τ''[bv::=b']_b[x::=v]_v = τ'› b_of_subst_bb_commute subst_tbase_eq  subst_b_b_def subst_v_τ_def subst_b_τ_def by auto
  ultimately show ?case using infer_e_appI by auto
next
  case (infer_e_fstI Θ B Γ Δ' Φ v z' b1 b2 c z)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_sndI Θ B Γ Δ' Φ v z' b1 b2 c z)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_lenI Θ B Γ Δ' Φ v z' c z)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_mvarI Θ Γ Φ Δ u τ)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_concatI Θ B Γ Δ' Φ v1 z1 c1 v2 z2 c2 z3)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_splitI Θ B Γ Δ Φ v1 z1 c1 v2 z2 z3)
  have " Θ ; Φ ; B ; Γ ; Δ ⊨_wf AE_split v1 v2 : B_pair B_bitvec B_bitvec"
  proof
    show "Θ ⊨_wf Φ" using infer_e_splitI by auto
    show "Θ; B; Γ ⊨_wf Δ" using infer_e_splitI by auto 
    show "Θ; B; Γ ⊨_wf v1 : B_bitvec" using infer_e_splitI b_of.simps infer_v_wf by metis
    show "Θ; B; Γ ⊨_wf v2 : B_int" using infer_e_splitI b_of.simps check_v_wf by metis
  qed  
  then show ?case using  b_of.simps by auto
qed

lemma infer_e_t_wf:
  fixes e::e and Γ::Γ and τ::τ and Δ::Δ and Φ::Φ
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ e ==> τ"
  shows "Θ; B;Γ ⊨_wf τ ∧ Θ ⊨_wf Φ" 
  using assms proof(induct  rule: infer_e.induct)
  case (infer_e_valI Θ B Γ Δ' Φ v τ)
  then show ?case using infer_v_t_wf by auto
next
  case (infer_e_plusI Θ B Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
  hence "Θ; B; Γ ⊨_wf CE_op Plus [v1]^ce [v2]^ce : B_int" using wfCE_plusI wfD_emptyI wfPhi_emptyI infer_v_v_wf  wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_plusI by auto
next
  case (infer_e_leqI Θ B Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
  hence " Θ; B; Γ ⊨_wf CE_op LEq [v1]^ce [v2]^ce : B_bool" using wfCE_leqI wfD_emptyI wfPhi_emptyI infer_v_v_wf wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_leqI by auto
next
  case (infer_e_eqI Θ B Γ Δ Φ v1 z1 b c1 v2 z2 c2 z3)
  hence " Θ; B; Γ ⊨_wf CE_op Eq [v1]^ce [v2]^ce : B_bool" using wfCE_eqI wfD_emptyI wfPhi_emptyI infer_v_v_wf wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_eqI by auto
next
  case (infer_e_appI Θ B Γ Δ Φ f x b c τ s' v τ')
  show ?case proof
    show "Θ ⊨_wf Φ" using infer_e_appI by auto
    show "Θ; B; Γ ⊨_wf τ'" proof -
      have *:" Θ; B; Γ ⊨_wf v : b " using infer_e_appI check_v_wf(2) b_of.simps by metis
      moreover have *:"Θ; B; (x, b, c) #_\<Gamma> Γ ⊨_wf τ" proof(rule  wf_weakening1(4))
        show ‹ Θ; B; (x,b,c)#_\ΓGNil ⊨_wf τ › using  wfPhi_f_simple_wfT wfD_wf infer_e_appI wb_b_weakening by fastforce
        have "Θ ; B ; Γ ⊨_wf { x : b | c }" using infer_e_appI check_v_wf(3) by auto
        thus  ‹ Θ ; B ⊨_wf (x, b, c) #_\Γ Γ › using infer_e_appI 
            wfT_wfC[THEN wfG_consI[rotated 3] ]  *  wfT_wf_cons fresh_prodN by simp
        show ‹toSet ((x,b,c)#_\ΓGNil) ⊆ toSet ((x, b, c) #_\Γ Γ)› using toSet.simps by auto
      qed
      moreover have "((x, b, c) #_\<Gamma> Γ)[x::=v]_\<Gamma>_v = Γ" using subst_gv.simps by auto

      ultimately show ?thesis using infer_e_appI wf_subst1(4)[OF *, of GNil x b c Γ v] subst_v_τ_def by auto
    qed
  qed
next
  case (infer_e_appPI Θ B Γ Δ Φ b' f bv x b c τ' s' v τ)

  have "Θ; B; ((x, b[bv::=b']_bb, c[bv::=b']_cb) #_\<Gamma> Γ)[x::=v]_\<Gamma>_v ⊨_wf (τ'[bv::=b']_b)[x::=v]_\<tau>_v" 
  proof(rule wf_subst(4))
    show ‹ Θ; B; (x, b[bv::=b']_bb, c[bv::=b']_cb) #_\Γ Γ ⊨_wf τ'[bv::=b']_b ›  
    proof(rule  wf_weakening1(4))
      have  ‹ Θ ; {|bv|} ; (x,b,c)#_\ΓGNil ⊨_wf τ' › using  wfPhi_f_poly_wfT  infer_e_appI infer_e_appPI by simp
      thus  ‹ Θ; B; (x,b[bv::=b']_bb,c[bv::=b']_cb)#_\ΓGNil ⊨_wf τ'[bv::=b']_b ›
        using wfT_subst_wfT infer_e_appPI wb_b_weakening subst_b_τ_def subst_v_τ_def by presburger
      have "Θ; B; Γ ⊨_wf { x : b[bv::=b']_bb | c[bv::=b']_cb }" 
        using infer_e_appPI check_v_wf(3) subst_b_b_def subst_b_c_def by metis
      thus  ‹ Θ ; B ⊨_wf (x, b[bv::=b']_bb, c[bv::=b']_cb) #_\Γ Γ ›
        using infer_e_appPI wfT_wfC[THEN wfG_consI[rotated 3] ]  * wfX_wfY wfT_wf_cons wb_b_weakening by metis
      show ‹toSet ((x,b[bv::=b']_bb,c[bv::=b']_cb)#_\ΓGNil) ⊆ toSet ((x, b[bv::=b']_bb, c[bv::=b']_cb) #_\Γ Γ)› using toSet.simps by auto
    qed
    show ‹(x, b[bv::=b']_bb, c[bv::=b']_cb) #_\Γ Γ = GNil @ (x, b[bv::=b']_bb, c[bv::=b']_cb) #_\Γ Γ› using append_g.simps by auto
    show ‹ Θ; B; Γ ⊨_wf v :b[bv::=b']_bb › using infer_e_appPI check_v_wf(2) b_of.simps subst_b_b_def by metis
  qed
  moreover have "((x, b[bv::=b']_bb, c[bv::=b']_cb) #_\<Gamma> Γ)[x::=v]_\<Gamma>_v = Γ" using subst_gv.simps by auto
  ultimately show ?case using infer_e_appPI subst_v_τ_def by simp
next
  case (infer_e_fstI Θ B Γ Δ Φ v z' b1 b2 c z)
  hence "Θ; B; Γ ⊨_wf CE_fst [v]^ce: b1" using wfCE_fstI wfD_emptyI wfPhi_emptyI infer_v_v_wf 
      b_of.simps  using wfCE_valI by fastforce
  then show ?case  using wfT_e_eq infer_e_fstI by auto
next
  case (infer_e_sndI Θ B Γ Δ Φ v z' b1 b2 c z)
  hence "Θ; B; Γ ⊨_wf CE_snd [v]^ce: b2" using wfCE_sndI wfD_emptyI wfPhi_emptyI infer_v_v_wf wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_sndI by auto
next
  case (infer_e_lenI Θ B Γ Δ Φ v z' c z)
  hence "Θ; B; Γ ⊨_wf CE_len [v]^ce: B_int" using wfCE_lenI wfD_emptyI wfPhi_emptyI infer_v_v_wf wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_lenI by auto
next
  case (infer_e_mvarI Θ Γ Φ Δ u τ)
  then show ?case using wfD_wfT by blast
next
  case (infer_e_concatI Θ B Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
  hence "Θ; B; Γ ⊨_wf CE_concat [v1]^ce [v2]^ce: B_bitvec" using wfCE_concatI wfD_emptyI wfPhi_emptyI infer_v_v_wf  wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_concatI by auto
next
  case (infer_e_splitI Θ B Γ Δ Φ v1 z1 c1 v2 z2 z3)

  hence wfg: " Θ ; B ⊨_wf (z3, [ B_bitvec , B_bitvec ]^b, TRUE) #_\<Gamma> Γ" 
    using infer_v_wf wfG_cons2I wfB_pairI wfB_bitvecI by simp
  have wfz: "Θ; B; (z3, [ B_bitvec , B_bitvec ]^b, TRUE) #_\<Gamma> Γ ⊨_wf [ [ z3 ]^v ]^ce : [ B_bitvec , B_bitvec ]^b "
    apply(rule wfCE_valI , rule wfV_varI)
    using wfg  apply simp
    using lookup.simps(2)[of z3 "[ B_bitvec , B_bitvec ]^b" TRUE Γ z3] by simp
  have 1: "Θ; B; (z3, [ B_bitvec , B_bitvec ]^b, TRUE) #_\<Gamma> Γ ⊨_wf [ v2 ]^ce : B_int " 
    using check_v_wf[OF infer_e_splitI(4)]  wf_weakening(1)[OF _ wfg] b_of.simps   toSet.simps wfCE_valI by fastforce
  have 2: "Θ; B; (z3, [ B_bitvec , B_bitvec ]^b, TRUE) #_\<Gamma> Γ ⊨_wf [ v1 ]^ce : B_bitvec" 
    using infer_v_wf[OF infer_e_splitI(3)]  wf_weakening(1)[OF _ wfg] b_of.simps   toSet.simps wfCE_valI by fastforce

  have "Θ; B; Γ ⊨_wf { z3 : [ B_bitvec , B_bitvec ]^b | [ v1 ]^ce == [ [#1[ [ z3 ]^v ]^ce]^ce @@ [#2[ [ z3 ]^v ]^ce]^ce ]^ce AND [| [#1[ [ z3 ]^v ]^ce]^ce |]^ce == [ v2 ]^ce }"
  proof
    show "atom z3 ♯ (Θ, B, Γ)" using infer_e_splitI wfTh_x_fresh wfX_wfY fresh_prod3 wfG_fresh_x by metis
    show "Θ ; B ⊨_wf [ B_bitvec , B_bitvec ]^b " using wfB_pairI wfB_bitvecI infer_e_splitI wfX_wfY by metis
    show "Θ; B; (z3, [ B_bitvec , B_bitvec ]^b, TRUE) #_\<Gamma>
              Γ ⊨_wf [ v1 ]^ce == [ [#1[ [ z3 ]^v ]^ce]^ce @@ [#2[ [ z3 ]^v ]^ce]^ce ]^ce AND [| [#1[ [ z3 ]^v ]^ce]^ce |]^ce == [ v2 ]^ce" 
      using wfg wfz 1 2 wf_intros by meson
  qed
  thus ?case using infer_e_splitI by auto
qed

lemma infer_e_wf:
  fixes e::e and Γ::Γ and τ::τ and Δ::Δ and Φ::Φ
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ e ==> τ"
  shows "Θ; B; Γ ⊨_wf τ" and "Θ ; B ⊨_wf Γ" and "Θ; B; Γ ⊨_wf Δ" and "Θ ⊨_wf Φ" and "Θ ; Φ ; B ; Γ ; Δ ⊨_wf e : (b_of τ)"
  using infer_e_t_wf infer_e_e_wf wfE_wf  assms by metis+

lemma infer_e_fresh:
  fixes x::x
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ e ==> τ" and "atom x ♯ Γ"
  shows "atom x ♯ (e,τ)"
proof - 
  have "atom x ♯ e" using infer_e_e_wf[THEN wfE_x_fresh,OF assms(1)] assms(2) by auto
  moreover have "atom x ♯ τ" using assms infer_e_wf  wfT_x_fresh by metis
  ultimately show ?thesis using fresh_Pair by auto
qed

inductive check_e :: "Θ ==> Φ ==> B ==> Γ ==> Δ ==> e ==> τ ==> bool"  (‹ _ ; _ ; _ ; _ ; _ ⊨ _ <== _› [50, 50, 50] 50) where
  check_e_subtypeI: "[ infer_e T P B G D e τ' ; subtype T B G τ' τ ] ==> check_e T P B G D e τ"
equivariance check_e
nominal_inductive check_e  .

inductive_cases check_e_elims[elim!]:
  "check_e F D B G Θ (AE_val v) τ"
  "check_e F D B G Θ e τ"

lemma infer_e_fst_pair:
  fixes v1::v
  assumes "Θ ; Φ ; {||} ; GNil ; Δ ⊨ [#1[ v1 , v2 ]^v]^e ==> τ"
  shows "∃τ'. Θ ; Φ ; {||} ; GNil ; Δ ⊨ [v1]^e ==> τ' ∧
        Θ ; {||} ; GNil ⊨ τ' < τ"
proof -
  obtain z' and b1 and b2 and c and z where ** : "τ = ({ z : b1 | C_eq (CE_val (V_var z)) (CE_fst [(V_pair v1 v2)]^ce) }) ∧
          wfD Θ {||} GNil Δ ∧ wfPhi Θ Φ ∧
              (Θ ; {||} ; GNil ⊨ V_pair v1 v2 ==> { z' : B_pair b1 b2 | c }) ∧ atom z ♯ V_pair v1 v2 "
    using infer_e_elims assms  by metis
  hence *:" Θ ; {||} ; GNil ⊨ V_pair v1 v2 ==> { z' : B_pair b1 b2 | c }" by auto

  obtain  t1a  and t2a  where
    *: "Θ ; {||} ; GNil ⊨ v1 ==> t1a ∧ Θ ; {||} ; GNil ⊨ v2 ==> t2a ∧ B_pair b1 b2 = B_pair (b_of t1a) (b_of t2a)"
    using infer_v_elims(5)[OF *] by metis

  hence  suppv: "supp v1 = {} ∧ supp v2 = {} ∧ supp (V_pair v1 v2) = {}" using ** infer_v_v_wf wfV_supp atom_dom.simps toSet.simps supp_GNil  
    by (meson wfV_supp_nil)

  obtain z1 and b1' where "t1a = { z1 : b1' | [ [ z1 ]^v ]^ce == [ v1 ]^ce } " 
    using infer_v_form[of Θ "{||}" GNil v1 t1a] * by auto
  moreover hence "b1' = b1" using * b_of.simps by simp
  ultimately have  "Θ ; {||} ; GNil ⊨ v1 ==> { z1 : b1 | CE_val (V_var z1) == CE_val v1 }" using * by auto
  moreover have "Θ ; {||} ; GNil ⊨_wf CE_fst [V_pair v1 v2]^ce : b1" using wfCE_fstI infer_v_wf(1) ** b_of.simps wfCE_valI by metis
  moreover hence st: "Θ ; {||} ; GNil ⊨ { z1 : b1 | CE_val (V_var z1) == CE_val v1 } < ({ z : b1 | CE_val (V_var z) == CE_fst [V_pair v1 v2]^ce })" 
    using subtype_gnil_fst infer_v_v_wf by auto
  moreover have "wfD Θ {||} GNil Δ ∧ wfPhi Θ Φ" using **  by auto
  ultimately show ?thesis  using wfX_wfY  ** infer_e_valI by metis
qed

lemma infer_e_snd_pair:
  assumes  "Θ ; Φ ; {||} ; GNil ; Δ ⊨ AE_snd (V_pair v1 v2) ==> τ"
  shows  "∃τ'. Θ ; Φ ; {||} ; GNil ; Δ ⊨ AE_val v2 ==> τ' ∧ Θ ; {||} ; GNil ⊨ τ' < τ"
proof -
  obtain z' and b1 and b2 and c and z where ** : "(τ = ({ z : b2 | C_eq (CE_val (V_var z)) (CE_snd [(V_pair v1 v2)]^ce) })) ∧
           (wfD Θ {||} GNil Δ) ∧ (wfPhi Θ Φ) ∧
              Θ ; {||} ; GNil ⊨ V_pair v1 v2 ==> { z' : B_pair b1 b2 | c } ∧ atom z ♯ V_pair v1 v2 "
    using infer_e_elims(9)[OF assms(1)]  by metis
  hence *:" Θ ; {||} ; GNil ⊨ V_pair v1 v2 ==> { z' : B_pair b1 b2 | c }" by auto

  obtain  t1a  and t2a  where
    *: "Θ ; {||} ; GNil ⊨ v1 ==> t1a ∧ Θ ; {||} ; GNil ⊨ v2 ==> t2a ∧ B_pair b1 b2 = B_pair (b_of t1a) (b_of t2a)"
    using infer_v_elims(5)[OF *] by metis

  hence  suppv: "supp v1 = {} ∧ supp v2 = {} ∧ supp (V_pair v1 v2) = {}" using infer_v_v_wf wfV.simps v.supp  by (meson "**" wfV_supp_nil)

  obtain z2 and b2' where "t2a = { z2 : b2' | [ [ z2 ]^v ]^ce == [ v2 ]^ce } " 
    using infer_v_form[of Θ "{||}" GNil v2 t2a] * by auto
  moreover hence "b2' = b2" using * b_of.simps by simp

  ultimately have  "Θ ; {||} ; GNil ⊨ v2 ==> { z2 : b2 | CE_val (V_var z2) == CE_val v2 }" using * by auto
  moreover have "Θ ; {||} ; GNil ⊨_wf CE_snd [V_pair v1 v2]^ce : b2" using wfCE_sndI infer_v_wf(1) ** b_of.simps wfCE_valI by metis
  moreover hence st: "Θ ; {||} ; GNil ⊨ { z2 : b2 | CE_val (V_var z2) == CE_val v2 } < ({ z : b2 | CE_val (V_var z) == CE_snd [V_pair v1 v2]^ce })" 
    using subtype_gnil_snd infer_v_v_wf by auto
  moreover have "wfD Θ {||} GNil Δ ∧ wfPhi Θ Φ" using ** by metis
  ultimately show ?thesis  using wfX_wfY  ** infer_e_valI by metis
qed

section ‹Statements›

lemma check_s_v_unit:
  assumes "Θ; B; Γ ⊨ ({ z : B_unit | TRUE }) < τ"  and "wfD Θ B Γ Δ" and "wfPhi Θ Φ"
  shows  "Θ ; Φ ; B ; Γ ; Δ ⊨ AS_val (V_lit L_unit ) <== τ" 
proof - 
  have "wfG Θ B Γ" using assms subtype_g_wf by meson
  moreover hence "wfTh Θ" using wfG_wf by simp
  moreover obtain z'::x where "atom z' ♯ Γ" using obtain_fresh by auto
  ultimately have *:"Θ; B; Γ ⊨ V_lit L_unit ==> { z' : B_unit | CE_val (V_var z') == CE_val (V_lit L_unit) }" 
    using infer_v_litI infer_unitI by simp
  moreover have "wfT Θ B Γ ({ z' : B_unit | CE_val (V_var z') == CE_val (V_lit L_unit) })" using infer_v_t_wf
    by (meson calculation)
  moreover then have  "Θ; B; Γ ⊨ ({ z' : B_unit | CE_val (V_var z') == CE_val (V_lit L_unit) }) < τ" using subtype_trans subtype_top assms 
      type_for_lit.simps(4) wfX_wfY by metis
  ultimately show  ?thesis using  check_valI assms * by auto
qed

lemma check_s_check_branch_s_wf:
  fixes s::s and cs::branch_s and Θ::Θ and Φ::Φ and Γ::Γ and Δ::Δ and v::v and τ::τ and css::branch_list
  shows "Θ ; Φ ; B ; Γ ; Δ ⊨ s <== τ ==> Θ ; B ⊨_wf Γ ∧ wfTh Θ ∧ wfD Θ B Γ Δ ∧ wfT Θ B Γ τ ∧ wfPhi Θ Φ " and 
    "check_branch_s Θ Φ B Γ Δ tid cons const v cs τ ==> Θ ; B ⊨_wf Γ ∧ wfTh Θ ∧ wfD Θ B Γ Δ ∧ wfT Θ B Γ τ ∧ wfPhi Θ Φ "
    "check_branch_list Θ Φ B Γ Δ tid dclist v css τ ==> Θ ; B ⊨_wf Γ ∧ wfTh Θ ∧ wfD Θ B Γ Δ ∧ wfT Θ B Γ τ ∧ wfPhi Θ Φ " 
proof(induct rule: check_s_check_branch_s_check_branch_list.inducts)
  case (check_valI Θ B Γ Δ Φ v τ' τ)
  then show ?case using infer_v_wf  infer_v_wf subtype_wf wfX_wfY wfS_valI 
    by (metis subtype_eq_base2)
next
  case (check_letI x Θ Φ B Γ Δ e τ z s b c)
  then have *:"wfT Θ B ((x, b , c[z::=V_var x]_v) #_\<Gamma> Γ) τ" by force
  moreover have "atom x ♯ τ" using check_letI fresh_prodN by force
  ultimately have "Θ; B;Γ ⊨_wf τ" using wfT_restrict2 by force
  then show ?case  using check_letI  infer_e_wf wfS_letI wfX_wfY wfG_elims by metis
next
  case (check_assertI x Θ Φ B Γ Δ c τ s)
  then have *:"wfT Θ B ((x, B_bool , c) #_\<Gamma> Γ) τ" by force
  moreover have "atom x ♯ τ" using check_assertI fresh_prodN by force
  ultimately have "Θ; B;Γ ⊨_wf τ" using wfT_restrict2 by force
  then show ?case  using check_assertI   wfS_assertI wfX_wfY wfG_elims by metis
next
  case (check_branch_s_branchI Θ B Γ Δ τ cons const x v Φ s tid)
  then show ?case using wfX_wfY by metis
next
  case (check_branch_list_consI Θ Φ B Γ Δ tid dclist' v cs τ css )
  then show ?case using wfX_wfY by metis
next
  case (check_branch_list_finalI Θ Φ B Γ Δ tid dclist' v cs τ )
  then show ?case using wfX_wfY by metis
next
  case (check_ifI z Θ Φ B Γ Δ v s1 s2 τ)
  hence *:"wfT Θ B Γ ({ z : b_of τ | CE_val v == CE_val (V_lit L_false) IMP c_of τ z })" (is "wfT Θ B Γ ?tau") by auto
  hence "wfT Θ B Γ τ" using wfT_wfT_if1 check_ifI  fresh_prodN by metis
  hence " Θ; B; Γ ⊨_wf τ " using check_ifI b_of_c_of_eq fresh_prodN by auto
  thus ?case using check_ifI by metis
next
  case (check_let2I x Θ Φ B G Δ t s1 τ s2)
  then have "wfT Θ B ((x, b_of t, (c_of t x)) #_\<Gamma> G) τ" by fastforce
  moreover have "atom x ♯ τ" using check_let2I by force
  ultimately have "wfT Θ B G τ" using wfT_restrict2 by metis
  then show ?case using check_let2I by argo
next
  case (check_varI u Δ P G v τ' Φ s τ)
  then show ?case using wfG_elims wfD_elims 
      list.distinct list.inject by metis
next
  case (check_assignI Θ Φ B Γ Δ u τ v z τ')
  obtain z'::x where *:"atom z' ♯ Γ" using obtain_fresh by metis
  moreover have "{ z : B_unit | TRUE } = { z' : B_unit | TRUE }" by auto
  moreover hence "wfT Θ B Γ { z' : B_unit |TRUE }" using wfT_TRUE check_assignI check_v_wf * wfB_unitI wfG_wf by metis
  ultimately show ?case  using check_v.cases infer_v_wf  subtype_wf check_assignI wfT_wf check_v_wf wfG_wf
    by (meson subtype_wf)
next
  case (check_whileI Φ Δ G P s1 z s2 τ')
  then show ?case using subtype_wf subtype_wf by auto
next
  case (check_seqI Δ G P s1 z s2 τ)
  then show ?case by fast
next
  case (check_caseI Θ Φ B Γ Δ  dclist cs τ tid v z)
  then show ?case by fast
qed

lemma check_s_check_branch_s_wfS:
  fixes s::s and cs::branch_s and Θ::Θ and Φ::Φ and Γ::Γ and Δ::Δ and v::v and τ::τ and css::branch_list
  shows "Θ ; Φ ; B ; Γ ; Δ ⊨ s <== τ ==> Θ ; Φ ; B ; Γ ; Δ ⊨_wf s : b_of τ " and 
    "check_branch_s Θ Φ B Γ Δ tid cons const v cs τ ==> wfCS Θ Φ B Γ Δ tid cons const cs (b_of τ)"
    "check_branch_list Θ Φ B Γ Δ tid dclist v css τ ==> wfCSS Θ Φ B Γ Δ tid dclist css (b_of τ)" 
proof(induct rule: check_s_check_branch_s_check_branch_list.inducts)
  case (check_valI Θ B Γ Δ Φ v τ' τ)
  then show ?case using infer_v_wf  infer_v_wf subtype_wf wfX_wfY wfS_valI 
    by (metis subtype_eq_base2)
next
  case (check_letI x Θ Φ B Γ Δ e τ z s b c)
  show ?case proof
    show ‹ Θ ; Φ ; B ; Γ ; Δ ⊨_wf e : b › using infer_e_wf check_letI b_of.simps by metis
    show ‹ Θ ; Φ ; B ; (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b_of τ ›  
      using check_letI b_of.simps wf_replace_true2(2)[OF check_letI(5)]   append_g.simps by metis
    show ‹ Θ; B; Γ ⊨_wf Δ ›  using infer_e_wf check_letI b_of.simps by metis
    show ‹atom x ♯ (Φ, Θ, B, Γ, Δ, e, b_of τ)›
      apply(simp add: fresh_prodN, intro conjI)
      using  check_letI(1) fresh_prod7 by simp+ 
  qed
next
  case (check_assertI x Θ Φ B Γ Δ c τ s)
  show ?case proof

    show ‹ Θ ; Φ ; B ; (x, B_bool, c) #_\Γ Γ ; Δ ⊨_wf s : b_of τ › using check_assertI by auto
  next
    show ‹ Θ; B; Γ ⊨_wf c › using check_assertI by auto
  next
    show ‹ Θ; B; Γ ⊨_wf Δ › using check_assertI by auto
  next
    show ‹atom x ♯ (Φ, Θ, B, Γ, Δ, c, b_of τ, s)› using check_assertI by auto
  qed
next
  case (check_branch_s_branchI Θ B Γ Δ τ const x Φ tid cons v s)
  show ?case proof
    show ‹ Θ ; Φ ; B ; (x, b_of const, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b_of τ ›
      using wf_replace_true append_g.simps check_branch_s_branchI by metis
    show ‹atom x ♯ (Φ, Θ, B, Γ, Δ, Γ, const)›
      using wf_replace_true append_g.simps check_branch_s_branchI fresh_prodN by metis
    show ‹ Θ; B; Γ ⊨_wf Δ › using wf_replace_true append_g.simps check_branch_s_branchI by metis
  qed
next
  case (check_branch_list_consI Θ Φ B Γ Δ tid cons const v cs τ dclist css)
  then show ?case using wf_intros by metis
next
  case (check_branch_list_finalI Θ Φ B Γ Δ tid cons const v cs τ)
  then show ?case using wf_intros by metis
next
  case (check_ifI z Θ Φ B Γ Δ v s1 s2 τ)
  show ?case using wfS_ifI check_v_wf check_ifI b_of.simps by metis
next
  case (check_let2I x Θ Φ B G Δ t s1 τ s2)
  show ?case proof
    show ‹ Θ ; Φ ; B ; G ; Δ ⊨_wf s1 : b_of t ›  using check_let2I  b_of.simps by metis 
    show ‹ Θ; B; G ⊨_wf t ›  using  check_let2I check_s_check_branch_s_wf  by metis
    show ‹ Θ ; Φ ; B ; (x, b_of t, TRUE) #_\Γ G ; Δ ⊨_wf s2 : b_of τ ›  
      using check_let2I(5) wf_replace_true2(2) append_g.simps check_let2I by metis 
    show ‹atom x ♯ (Φ, Θ, B, G, Δ, s1, b_of τ, t)›  
      apply(simp add: fresh_prodN, intro conjI)
      using  check_let2I(1) fresh_prod7 by simp+ 
  qed
next
  case (check_varI u Θ Φ B Γ Δ τ' v τ s)
  show ?case proof
    show ‹ Θ; B; Γ ⊨_wf τ' › using check_v_wf check_varI by metis
    show ‹ Θ; B; Γ ⊨_wf v : b_of τ' ›  using check_v_wf check_varI by metis
    show ‹atom u ♯ (Φ, Θ, B, Γ, Δ, τ', v, b_of τ)›  using check_varI fresh_prodN u_fresh_b by metis
    show ‹ Θ ; Φ ; B ; Γ ; (u, τ') #_\ΔΔ ⊨_wf s : b_of τ ›  using check_varI by metis
  qed   
next
  case (check_assignI Θ Φ B Γ Δ u τ v z τ')
  then show ?case using wf_intros check_v_wf subtype_eq_base2 b_of.simps by metis
next
  case (check_whileI Θ Φ B Γ Δ s1 z s2 τ')
  thus ?case using wf_intros  b_of.simps  check_v_wf subtype_eq_base2 b_of.simps by metis
next
  case (check_seqI Θ Φ B Γ Δ s1 z s2 τ)
  thus ?case using wf_intros  b_of.simps  by metis
next
  case (check_caseI Θ Φ B Γ Δ tid dclist v cs τ z)
  show  ?case proof
    show ‹ Θ; B; Γ ⊨_wf v : B_id tid › using check_caseI check_v_wf b_of.simps  by metis
    show ‹AF_typedef tid dclist ∈ set Θ›  using check_caseI by metis
    show ‹ Θ; B; Γ ⊨_wf Δ ›  using check_caseI check_s_check_branch_s_wf by metis
    show ‹ Θ ⊨_wf Φ ›  using check_caseI check_s_check_branch_s_wf  by metis
    show ‹ Θ ; Φ ; B ; Γ ; Δ ; tid ; dclist ⊨_wf cs : b_of τ ›  using check_caseI by metis
  qed
qed

lemma check_s_wf:
  fixes s::s
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ s <== τ"
  shows "Θ ; B ⊨_wf Γ ∧ wfT Θ B Γ τ ∧ wfPhi Θ Φ ∧ wfTh Θ ∧ wfD Θ B Γ Δ ∧ wfS Θ Φ B Γ Δ s (b_of τ)"  
  using check_s_check_branch_s_wf check_s_check_branch_s_wfS assms  by meson

lemma check_s_flip_u1:
  fixes s::s and u::u and u'::u
  assumes  "Θ ; Φ ; B ; Γ ; Δ ⊨ s <== τ"
  shows "Θ ; Φ ; B ; Γ ; ( u ↔ u') ∙ Δ ⊨ (u ↔ u') ∙ s <== τ" 
proof - 
  have  "(u ↔ u') ∙ Θ ; (u ↔ u') ∙ Φ ; (u ↔ u') ∙ B ; (u ↔ u') ∙ Γ ; (u ↔ u') ∙ Δ ⊨ (u ↔ u') ∙ s <== (u ↔ u') ∙ τ" 
    using check_s.eqvt assms  by blast
  thus  ?thesis using check_s_wf[OF assms] flip_u_eq phi_flip_eq  by metis
qed

lemma check_s_flip_u2: 
  fixes s::s and u::u and u'::u
  assumes "Θ ; Φ ; B ; Γ ; ( u ↔ u') ∙ Δ ⊨ (u ↔ u') ∙ s <== τ" 
  shows "Θ ; Φ ; B ; Γ ; Δ ⊨ s <== τ"
proof - 
  have "Θ ; Φ ; B ; Γ ; ( u ↔ u') ∙ ( u ↔ u') ∙ Δ ⊨ ( u ↔ u') ∙ (u ↔ u') ∙ s <== τ" 
    using check_s_flip_u1 assms by blast
  thus ?thesis using  permute_flip_cancel by force
qed

lemma check_s_flip_u:
  fixes s::s and u::u and u'::u
  shows "Θ ; Φ ; B ; Γ ; ( u ↔ u') ∙ Δ ⊨ (u ↔ u') ∙ s <== τ = (Θ ; Φ ; B ; Γ ; Δ ⊨ s <== τ)"
  using check_s_flip_u1  check_s_flip_u2 by metis

lemma check_s_abs_u:
  fixes s::s and s'::s and u::u and u'::u and τ'::τ
  assumes "[[atom u]]lst. s = [[atom u']]lst. s'" and "atom u ♯ Δ" and "atom u' ♯ Δ"
    and "Θ ; B ; Γ ⊨_wf τ'" 
    and "Θ ; Φ ; B ; Γ ; ( u , τ') #_\<Delta>Δ ⊨ s <== τ"
  shows "Θ ; Φ ; B ; Γ ; ( u', τ' ) #_\<Delta>Δ ⊨ s' <== τ"
proof -
  have "Θ ; Φ ; B ; Γ ; ( u' ↔ u) ∙ (( u , τ') #_\<Delta>Δ) ⊨ ( u' ↔ u) ∙ s <== τ"
    using assms check_s_flip_u by metis
  moreover have " ( u' ↔ u) ∙ (( u , τ') #_\<Delta> Δ) = ( u' , τ') #_\<Delta>Δ" proof -
    have " ( u' ↔ u) ∙ (( u , τ') #_\<Delta> Δ) = ((u' ↔ u) ∙ u, (u' ↔ u) ∙ τ') #_\<Delta> (u' ↔ u) ∙ Δ"  
      using  DCons_eqvt  Pair_eqvt by auto
    also have "... = ( u' , (u' ↔ u) ∙ τ') #_\<Delta> Δ" 
      using assms flip_fresh_fresh by auto
    also have "... = ( u' , τ') #_\<Delta> Δ" using
        u_not_in_t fresh_def flip_fresh_fresh assms by metis
    finally show ?thesis by auto
  qed
  moreover have "( u' ↔ u) ∙ s = s'" using assms Abs1_eq_iff(3)[of u' s' u s] by auto
  ultimately show ?thesis by auto
qed

section ‹Additional Elimination and Intros›

subsection  ‹Values›

nominal_function b_for :: "opp ==> b" where
  "b_for Plus = B_int"
| "b_for LEq = B_bool" | "b_for Eq = B_bool"
  apply(auto,simp add: eqvt_def b_for_graph_aux_def )
  by (meson opp.exhaust)
nominal_termination (eqvt)  by lexicographic_order


lemma infer_v_pair2I:
  fixes  v₁::v and  v₂::v
  assumes "Θ; B; Γ ⊨ v₁ ==> τ₁" and "Θ; B; Γ ⊨ v₂ ==> τ₂"
  shows "∃τ. Θ; B; Γ ⊨ V_pair v₁ v₂ ==> τ ∧ b_of τ = B_pair (b_of τ₁) (b_of τ₂)"
proof - 
  obtain z1 and b1 and c1 and z2 and b2 and c2 where zbc: "τ₁ = ({ z1 : b1 | c1 }) ∧ τ₂ = ({ z2 : b2 | c2 })"
    using τ.exhaust by meson
  obtain z::x where "atom z ♯ ( v₁, v₂,Θ, B,Γ)" using obtain_fresh
    by blast
  hence "atom z ♯ ( v₁, v₂) ∧ atom z ♯ (Θ, B,Γ)" using fresh_prodN by metis
  hence " Θ; B; Γ ⊨ V_pair v₁ v₂ ==> { z : [ b_of τ₁ , b_of τ₂ ]^b | CE_val (V_var z) == CE_val (V_pair v₁ v₂) }"  
    using assms infer_v_pairI zbc by metis
  moreover obtain τ where "τ = ({ z : B_pair b1 b2 | CE_val (V_var z) == CE_val (V_pair v₁ v₂) })" by blast
  moreover hence "b_of τ = B_pair (b_of τ₁) (b_of τ₂)" using b_of.simps zbc by presburger
  ultimately show ?thesis using b_of.simps by metis
qed

lemma infer_v_pair2I_zbc:
  fixes  v₁::v and  v₂::v
  assumes "Θ; B; Γ ⊨ v₁ ==> τ₁" and "Θ; B; Γ ⊨ v₂ ==> τ₂"
  shows "∃z τ. Θ; B; Γ ⊨ V_pair v₁ v₂ ==> τ ∧ τ = ({ z : B_pair (b_of τ₁) (b_of τ₂) | C_eq (CE_val (V_var z)) (CE_val (V_pair v₁ v₂)) }) ∧ atom z ♯ (v₁,v₂) ∧ atom z ♯ Γ"
proof - 
  obtain z1 and b1 and c1 and z2 and b2 and c2 where zbc: "τ₁ = ({ z1 : b1 | c1 }) ∧ τ₂ = ({ z2 : b2 | c2 })"
    using τ.exhaust by meson
  obtain z::x where * : "atom z ♯ ( v₁, v₂,Γ,Θ , B )"  using obtain_fresh
    by blast
  hence vinf: " Θ; B; Γ ⊨ V_pair v₁ v₂ ==> { z :[ b_of τ₁ , b_of τ₂ ]^b | CE_val (V_var z) == CE_val (V_pair v₁ v₂) }"  
    using assms infer_v_pairI by simp
  moreover obtain τ where "τ = ({ z : B_pair b1 b2 | CE_val (V_var z) == CE_val (V_pair v₁ v₂) })" by blast
  moreover have "b_of τ₁ = b1 ∧ b_of τ₂ = b2" using zbc b_of.simps by auto
  ultimately have "Θ; B; Γ ⊨ V_pair v₁ v₂ ==> τ ∧ τ = ({ z : B_pair (b_of τ₁) (b_of τ₂) | CE_val (V_var z) == CE_val (V_pair v₁ v₂) })" by auto
  thus ?thesis using * fresh_prod2 fresh_prod3 by metis
qed

lemma infer_v_pair2E:
  assumes "Θ; B; Γ ⊨ V_pair v₁ v₂ ==> τ"
  shows "∃τ₁ τ₂ z . Θ; B; Γ ⊨ v₁ ==> τ₁ ∧ Θ; B; Γ ⊨ v₂ ==> τ₂ ∧
           τ = ({ z : B_pair (b_of τ₁) (b_of τ₂) | C_eq (CE_val (V_var z)) (CE_val (V_pair v₁ v₂)) }) ∧ atom z ♯ (v₁, v₂)" 
proof - 
  obtain z and t1 and t2 where 
    "τ = ({ z : B_pair (b_of t1) (b_of t2) | CE_val (V_var z) == CE_val (V_pair v₁ v₂) }) ∧
        atom z ♯ (v₁, v₂) ∧ Θ; B; Γ ⊨ v₁ ==> t1 ∧ Θ; B; Γ ⊨ v₂ ==> t2 " using infer_v_elims(3)[OF assms ] by metis 
  thus ?thesis using b_of.simps  by metis
qed

subsection  ‹Expressions›

lemma infer_e_app2E:
  fixes Φ::Φ and Θ::Θ
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ AE_app f v ==> τ"
  shows "∃x b c s' τ'. wfD Θ B Γ Δ ∧ Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ' s'))) = lookup_fun Φ f ∧ Θ ⊨_wf Φ ∧
       Θ; B; Γ ⊨ v <== { x : b | c } ∧ τ = τ'[x::=v]_\<tau>_v ∧ atom x ♯ (Θ, Φ, B, Γ, Δ, v, τ)"
  using infer_e_elims(6)[OF assms] b_of.simps subst_defs by metis

lemma infer_e_appP2E:
  fixes Φ::Φ and Θ::Θ
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ AE_appP f b v ==> τ"
  shows "∃bv x ba c s' τ'. wfD Θ B Γ Δ ∧ Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x ba c τ' s'))) = lookup_fun Φ f ∧ Θ ⊨_wf Φ ∧ Θ ; B ⊨_wf b ∧
      (Θ; B; Γ ⊨ v <== { x : ba[bv::=b]_bb | c[bv::=b]_cb }) ∧ (τ = τ'[bv::=b]_\<tau>_b[x::=v]_\<tau>_v) ∧ atom x ♯ Γ ∧ atom bv ♯ v"
proof -
  obtain bv x ba c s' τ' where *:"wfD Θ B Γ Δ ∧ Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x ba c τ' s'))) = lookup_fun Φ f ∧ Θ ⊨_wf Φ ∧ Θ ; B ⊨_wf b ∧
      (Θ; B; Γ ⊨ v <== { x : ba[bv::=b]_bb | c[bv::=b]_cb }) ∧ (τ = τ'[bv::=b]_\<tau>_b[x::=v]_\<tau>_v) ∧ atom x ♯ Γ ∧ atom bv ♯ (Θ, Φ, B, Γ, Δ, b, v, τ)" 
    using infer_e_elims(21)[OF assms] subst_defs by metis
  moreover then have "atom bv ♯ v" using fresh_prodN by metis
  ultimately show ?thesis by metis
qed

section ‹Weakening›

text ‹ Lemmas showing that typing judgements hold when a context is extended ›

lemma subtype_weakening:
  fixes Γ'::Γ
  assumes "Θ; B; Γ ⊨ τ1 < τ2" and  "toSet Γ ⊆ toSet Γ'" and "Θ ; B ⊨_wf Γ'" 
  shows  "Θ; B; Γ' ⊨ τ1 < τ2"
  using assms proof(nominal_induct τ2 avoiding: Γ' rule: subtype.strong_induct)

  case (subtype_baseI x Θ B Γ z c z' c' b)
  show ?case proof
    show *:"Θ; B; Γ' ⊨_wf { z : b | c }" using wfT_weakening subtype_baseI by metis
    show "Θ; B; Γ' ⊨_wf { z' : b | c' }" using wfT_weakening subtype_baseI by metis
    show "atom x ♯ (Θ, B, Γ', z , c , z' , c' )" using subtype_baseI fresh_Pair by metis
    have "toSet ((x, b, c[z::=V_var x]_v) #_\<Gamma> Γ) ⊆ toSet ((x, b, c[z::=V_var x]_v) #_\<Gamma> Γ')" using subtype_baseI toSet.simps by blast
    moreover have "Θ ; B ⊨_wf (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ'" using wfT_wf_cons3[OF *, of x] subtype_baseI fresh_Pair subst_defs by metis
    ultimately show "Θ; B; (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ' ⊨ c'[z'::=V_var x]_v" using valid_weakening subtype_baseI by metis
  qed
qed

method many_rules uses add = ( (rule+),((simp add: add)+)?)

lemma infer_v_g_weakening:
  fixes e::e and Γ'::Γ and v::v
  assumes "Θ; B ; Γ ⊨ v ==> τ" and "toSet Γ ⊆ toSet Γ'" and "Θ ; B ⊨_wf Γ'"
  shows   "Θ; B ; Γ' ⊨ v ==> τ"
  using assms proof(nominal_induct   avoiding: Γ'  rule: infer_v.strong_induct)
  case (infer_v_varI Θ B Γ b c x' z)  
  show ?case proof
    show ‹ Θ ; B ⊨_wf Γ' › using infer_v_varI by auto
    show ‹Some (b, c) = lookup Γ' x'› using infer_v_varI lookup_weakening by metis
    show ‹atom z ♯ x'› using infer_v_varI by auto
    show ‹atom z ♯ (Θ, B, Γ')› using infer_v_varI by auto
  qed
next
  case (infer_v_litI Θ B Γ l τ)
  then show ?case using infer_v.intros by simp
next
  case (infer_v_pairI z v1 v2 Θ B Γ t1 t2)
  then show ?case using infer_v.intros by simp
next
  case (infer_v_consI s dclist Θ dc tc B Γ 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 ‹ Θ; B; Γ' ⊨ v ==> tv› using infer_v_consI by auto
    show ‹Θ; B; Γ' ⊨ tv < tc› using infer_v_consI subtype_weakening by auto
    show ‹atom z ♯ v› using infer_v_consI by auto
    show ‹atom z ♯ (Θ, B, Γ')› using infer_v_consI by auto
  qed
next
  case (infer_v_conspI s bv dclist Θ dc tc B Γ 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 ‹ Θ; B; Γ' ⊨ v ==> tv› using infer_v_conspI by auto
    show ‹Θ; B; Γ' ⊨ tv < tc[bv::=b]_\τ_b› using infer_v_conspI subtype_weakening by auto
    show ‹atom z ♯ (Θ, B, Γ', v, b)› using infer_v_conspI by auto
    show ‹atom bv ♯ (Θ, B, Γ', v, b)› using infer_v_conspI by auto
    show ‹ Θ ; B ⊨_wf b › using infer_v_conspI by auto
  qed
qed

lemma check_v_g_weakening:
  fixes e::e and Γ'::Γ
  assumes "Θ; B ; Γ ⊨ v <== τ" and "toSet Γ ⊆ toSet Γ'" and "Θ ; B ⊨_wf Γ'" 
  shows   "Θ; B ; Γ' ⊨ v <== τ"
  using subtype_weakening infer_v_g_weakening check_v_elims  check_v_subtypeI assms by metis

lemma infer_e_g_weakening:
  fixes e::e and Γ'::Γ
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ e ==> τ" and "toSet Γ ⊆ toSet Γ'" and "Θ ; B ⊨_wf Γ'"
  shows   "Θ ; Φ ; B ; Γ'; Δ ⊨ e ==> τ"
  using assms proof(nominal_induct τ avoiding: Γ'  rule: infer_e.strong_induct)
  case (infer_e_valI Θ B Γ Δ' Φ v τ)
  then show ?case using infer_v_g_weakening wf_weakening infer_e.intros by metis
next
  case (infer_e_plusI Θ  B Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)

  obtain z'::x where z': "atom z' ♯ v1 ∧ atom z' ♯ v2 ∧ atom z' ♯ Γ'" using obtain_fresh fresh_prod3 by metis
  moreover hence  *:"{ z3 : B_int | CE_val (V_var z3) == CE_op Plus [v1]^ce [v2]^ce } = ({ z' : B_int | CE_val (V_var z') == CE_op Plus [v1]^ce [v2]^ce })" 
    using infer_e_plusI type_e_eq ce.fresh fresh_e_opp by auto

  have "Θ ; Φ ; B ; Γ' ; Δ ⊨ AE_op Plus v1 v2 ==> { z' : B_int | CE_val (V_var z') == CE_op Plus [v1]^ce [v2]^ce }" proof
    show ‹ Θ ; B ; Γ' ⊨_wf Δ › using wf_weakening infer_e_plusI by auto
    show ‹ Θ ⊨_wf Φ › using infer_e_plusI by auto
    show ‹ Θ ; B ; Γ' ⊨ v1 ==> { z1 : B_int | c1 }› using infer_v_g_weakening infer_e_plusI by auto
    show ‹ Θ ; B ; Γ' ⊨ v2 ==> { z2 : B_int | c2 }› using infer_v_g_weakening infer_e_plusI by auto
    show ‹atom z' ♯ AE_op Plus v1 v2› using z'  by auto
    show ‹atom z' ♯ Γ'› using z' by auto
  qed
  thus ?case using * by metis

next
  case (infer_e_leqI Θ B Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
  obtain z'::x where z': "atom z' ♯ v1 ∧ atom z' ♯ v2 ∧ atom z' ♯ Γ'" using obtain_fresh fresh_prod3 by metis

  moreover hence  *:"{ z3 : B_bool | CE_val (V_var z3) == CE_op LEq [v1]^ce [v2]^ce } = ({ z' : B_bool | CE_val (V_var z') == CE_op LEq [v1]^ce [v2]^ce })" 
    using infer_e_leqI type_e_eq ce.fresh fresh_e_opp by auto

  have "Θ ; Φ ; B ; Γ' ; Δ ⊨ AE_op LEq v1 v2 ==> { z' : B_bool | CE_val (V_var z') == CE_op LEq [v1]^ce [v2]^ce }" proof
    show ‹ Θ ; B ; Γ' ⊨_wf Δ › using wf_weakening infer_e_leqI by auto
    show ‹ Θ ⊨_wf Φ › using infer_e_leqI by auto
    show ‹ Θ ; B ; Γ' ⊨ v1 ==> { z1 : B_int | c1 }› using infer_v_g_weakening infer_e_leqI by auto
    show ‹ Θ ; B ; Γ' ⊨ v2 ==> { z2 : B_int | c2 }› using infer_v_g_weakening infer_e_leqI by auto
    show ‹atom z' ♯ AE_op LEq v1 v2› using z'  by auto
    show ‹atom z' ♯ Γ'› using z' by auto
  qed
  thus ?case using * by metis
next
  case (infer_e_eqI Θ B Γ Δ Φ v1 z1 bb c1 v2 z2 c2 z3)
  obtain z'::x where z': "atom z' ♯ v1 ∧ atom z' ♯ v2 ∧ atom z' ♯ Γ'" using obtain_fresh fresh_prod3 by metis

  moreover hence  *:"{ z3 : B_bool | CE_val (V_var z3) == CE_op Eq [v1]^ce [v2]^ce } = ({ z' : B_bool | CE_val (V_var z') == CE_op Eq [v1]^ce [v2]^ce })" 
    using infer_e_eqI type_e_eq ce.fresh fresh_e_opp by auto

  have "Θ ; Φ ; B ; Γ' ; Δ ⊨ AE_op Eq v1 v2 ==> { z' : B_bool | CE_val (V_var z') == CE_op Eq [v1]^ce [v2]^ce }" proof
    show ‹ Θ ; B ; Γ' ⊨_wf Δ › using wf_weakening infer_e_eqI by auto
    show ‹ Θ ⊨_wf Φ › using infer_e_eqI by auto
    show ‹ Θ ; B ; Γ' ⊨ v1 ==> { z1 : bb | c1 }› using infer_v_g_weakening infer_e_eqI by auto
    show ‹ Θ ; B ; Γ' ⊨ v2 ==> { z2 : bb | c2 }› using infer_v_g_weakening infer_e_eqI by auto
    show ‹atom z' ♯ AE_op Eq v1 v2› using z'  by auto
    show ‹atom z' ♯ Γ'› using z' by auto
    show "bb ∈ {B_bool, B_int, B_unit}" using infer_e_eqI by auto
  qed
  thus ?case using * by metis
next
  case (infer_e_appI Θ B Γ Δ Φ f x b c τ' s' v τ)
  show ?case proof 
    show "Θ; B; Γ' ⊨_wf Δ "  using wf_weakening infer_e_appI by auto
    show "Θ ⊨_wf Φ"   using wf_weakening 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 wf_weakening infer_e_appI by auto
    show "Θ; B; Γ' ⊨ v <== { x : b | c }"  using wf_weakening infer_e_appI check_v_g_weakening by auto
    show "atom x ♯ (Θ, Φ, B, Γ', Δ, v, τ)"  using wf_weakening infer_e_appI by auto
    show "τ'[x::=v]_v = τ"  using wf_weakening infer_e_appI by auto
  qed

next
  case (infer_e_appPI Θ B Γ Δ Φ b' f bv x b c τ' s' v τ)

  hence *:"Θ ; Φ ; B ; Γ ; Δ ⊨ AE_appP f b' v ==> τ" using Typing.infer_e_appPI by auto

  obtain x'::x where x':"atom x' ♯ (s', c, τ', (Γ',v,τ)) ∧ (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c τ' s'))) = (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x' b ((x' ↔ x) ∙ c) ((x' ↔ x) ∙ τ') ((x' ↔ x) ∙ s'))))" 
    using obtain_fresh_fun_def[of s' c τ' "(Γ',v,τ)" f x b]
    by (metis fun_def.eq_iff fun_typ_q.eq_iff(2))

  hence **: " { x : b | c } = { x' : b | (x' ↔ x) ∙ c }" 
    using fresh_PairD(1) fresh_PairD(2) type_eq_flip by blast
  have "atom x' ♯ Γ" using x' infer_e_appPI fresh_weakening fresh_Pair by metis

  show ?case proof(rule Typing.infer_e_appPI[where x=x' and bv=bv and b=b and c="(x' ↔ x) ∙ c" and τ'="(x' ↔ x) ∙ τ'"and s'="((x' ↔ x) ∙ s')"])
    show ‹ Θ ; B ; Γ' ⊨_wf Δ › using wf_weakening infer_e_appPI by auto
    show ‹ Θ ⊨_wf Φ › using wf_weakening infer_e_appPI by auto
    show "Θ ; B ⊨_wf b'" using infer_e_appPI by auto
    show "Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x' b ((x' ↔ x) ∙ c) ((x' ↔ x) ∙ τ') ((x' ↔ x) ∙ s')))) = lookup_fun Φ f" using x' infer_e_appPI by argo
    show "Θ; B; Γ' ⊨ v <== { x' : b[bv::=b']_b | ((x' ↔ x) ∙ c)[bv::=b']_b }" using **
        τ.eq_iff check_v_g_weakening infer_e_appPI.hyps infer_e_appPI.prems(1) infer_e_appPI.prems subst_defs
        subst_tb.simps by metis
    show "atom x' ♯ Γ'" using x' fresh_prodN by metis

    have "atom x ♯ (v, τ) ∧ atom x' ♯ (v, τ)" using x' infer_e_fresh[OF *] e.fresh(2) fresh_Pair infer_e_appPI ‹atom x' ♯ Γ› e.fresh by metis
    moreover then have "((x' ↔ x) ∙ τ')[bv::=b']_\<tau>_b = (x' ↔ x) ∙ (τ'[bv::=b']_\<tau>_b)" using  subst_b_x_flip 
      by (metis subst_b_τ_def)
    ultimately show "((x' ↔ x) ∙ τ')[bv::=b']_b[x'::=v]_v = τ" 
      using infer_e_appPI subst_tv_flip subst_defs by metis

    show "atom bv ♯ (Θ, Φ, B, Γ', Δ, b', v, τ)" using infer_e_appPI fresh_prodN by metis
  qed

next
  case (infer_e_fstI Θ  B Γ Δ Φ v z'' b1 b2 c z)

  obtain z'::x where  *: "atom z' ♯ Γ' ∧ atom z' ♯ v ∧ atom z' ♯ c" using obtain_fresh_z fresh_Pair by metis 
  hence **:"{ z : b1 | CE_val (V_var z) == CE_fst [v]^ce } = { z' : b1 | CE_val (V_var z') == CE_fst [v]^ce }"
    using  type_e_eq infer_e_fstI v.fresh e.fresh ce.fresh obtain_fresh_z fresh_Pair by metis

  have "Θ ; Φ ; B ; Γ' ; Δ ⊨ AE_fst v ==> { z' : b1 | CE_val (V_var z') == CE_fst [v]^ce }" proof
    show ‹ Θ ; B ; Γ' ⊨_wf Δ › using wf_weakening infer_e_fstI by auto
    show ‹ Θ ⊨_wf Φ › using wf_weakening infer_e_fstI by auto
    show "Θ ; B ; Γ' ⊨ v ==> { z'' : B_pair b1 b2 | c }" using infer_v_g_weakening infer_e_fstI  by metis
    show "atom z' ♯ AE_fst v" using * ** e.supp by auto
    show "atom z' ♯ Γ'" using * by auto
  qed
  thus ?case using * ** by metis
next
  case (infer_e_sndI Θ  B Γ Δ Φ v z'' b1 b2 c z)

  obtain z'::x where  *: "atom z' ♯ Γ' ∧ atom z' ♯ v ∧ atom z' ♯ c"  using obtain_fresh_z fresh_Pair by metis 
  hence **:"{ z : b2 | CE_val (V_var z) == CE_snd [v]^ce } = { z' : b2 | CE_val (V_var z') == CE_snd [v]^ce }"
    using  type_e_eq infer_e_sndI e.fresh ce.fresh obtain_fresh_z fresh_Pair by metis

  have "Θ ; Φ ; B ; Γ' ; Δ ⊨ AE_snd v ==> { z' : b2 | CE_val (V_var z') == CE_snd [v]^ce }" proof
    show ‹ Θ ; B ;Γ' ⊨_wf Δ › using wf_weakening infer_e_sndI by auto
    show ‹ Θ ⊨_wf Φ › using wf_weakening infer_e_sndI by auto
    show "Θ ; B ; Γ' ⊨ v ==> { z'' : B_pair b1 b2 | c }" using infer_v_g_weakening infer_e_sndI    by metis
    show "atom z' ♯ AE_snd v" using * e.supp by auto
    show "atom z' ♯ Γ'" using * by auto
  qed
  thus ?case using ** by metis
next
  case (infer_e_lenI Θ  B Γ Δ Φ v z'' c z)

  obtain z'::x where  *: "atom z' ♯ Γ' ∧ atom z' ♯ v ∧ atom z' ♯ c"  using obtain_fresh_z fresh_Pair by metis 
  hence **:"{ z : B_int | CE_val (V_var z) == CE_len [v]^ce } = { z' : B_int | CE_val (V_var z') == CE_len [v]^ce }"
    using  type_e_eq infer_e_lenI e.fresh ce.fresh obtain_fresh_z fresh_Pair by metis

  have "Θ ; Φ ; B ; Γ' ; Δ ⊨ AE_len v ==> { z' : B_int | CE_val (V_var z') == CE_len [v]^ce }" proof
    show ‹ Θ; B; Γ' ⊨_wf Δ › using wf_weakening infer_e_lenI by auto
    show ‹ Θ ⊨_wf Φ › using wf_weakening infer_e_lenI by auto
    show "Θ ; B ; Γ' ⊨ v ==> { z'' : B_bitvec | c }" using infer_v_g_weakening infer_e_lenI    by metis
    show "atom z' ♯ AE_len v" using * e.supp by auto
    show "atom z' ♯ Γ'" using * by auto
  qed
  thus ?case using * ** by metis
next
  case (infer_e_mvarI Θ Γ Φ Δ u τ)
  then show ?case using  wf_weakening infer_e.intros by metis
next
  case (infer_e_concatI Θ  B Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)

  obtain z'::x where  *: "atom z' ♯ Γ' ∧ atom z' ♯ v1 ∧ atom z' ♯ v2" using obtain_fresh_z fresh_Pair by metis 
  hence **:"{ z3 : B_bitvec | CE_val (V_var z3) == CE_concat [v1]^ce [v2]^ce } = { z' : B_bitvec | CE_val (V_var z') == CE_concat [v1]^ce [v2]^ce }"
    using  type_e_eq infer_e_concatI e.fresh ce.fresh obtain_fresh_z fresh_Pair by metis

  have "Θ ; Φ ; B ; Γ' ; Δ ⊨ AE_concat v1 v2 ==> { z' : B_bitvec | CE_val (V_var z') == CE_concat [v1]^ce [v2]^ce }" proof
    show ‹ Θ; B; Γ' ⊨_wf Δ › using wf_weakening infer_e_concatI by auto
    show ‹ Θ ⊨_wf Φ › using wf_weakening infer_e_concatI by auto
    show "Θ ; B ; Γ' ⊨ v1 ==> { z1 : B_bitvec | c1 }" using infer_v_g_weakening infer_e_concatI    by metis
    show "Θ ; B ; Γ' ⊨ v2 ==> { z2 : B_bitvec | c2 }" using infer_v_g_weakening infer_e_concatI    by metis
    show "atom z' ♯ AE_concat v1 v2" using * e.supp by auto
    show "atom z' ♯ Γ'" using * by auto
  qed
  thus ?case using * ** by metis
next
  case (infer_e_splitI Θ B Γ Δ Φ v1 z1 c1 v2 z2 z3)
  show ?case proof
    show "Θ; B; Γ' ⊨_wf Δ" using infer_e_splitI wf_weakening by auto
    show "Θ ⊨_wf Φ " using infer_e_splitI wf_weakening by auto
    show "Θ; B; Γ' ⊨ v1 ==> { z1 : B_bitvec | c1 }" using infer_v_g_weakening infer_e_splitI by metis
    show "Θ; B; Γ' ⊨ v2 <== { z2 : B_int | [ leq [ [ L_num 0 ]^v ]^ce [ [ z2 ]^v ]^ce ]^ce == [ [ L_true ]^v ]^ce
                  AND [ leq [ [ z2 ]^v ]^ce [| [ v1 ]^ce |]^ce ]^ce == [ [ L_true ]^v ]^ce }" 
      using check_v_g_weakening infer_e_splitI by metis
    show "atom z1 ♯ AE_split v1 v2" using infer_e_splitI by auto
    show "atom z1 ♯ Γ'" using infer_e_splitI by auto
    show "atom z2 ♯ AE_split v1 v2" using infer_e_splitI by auto
    show "atom z2 ♯ Γ'" using infer_e_splitI by auto
    show "atom z3 ♯ AE_split v1 v2" using infer_e_splitI by auto
    show "atom z3 ♯ Γ'" using infer_e_splitI by auto
  qed
qed

text ‹ Special cases proved explicitly, other cases at the end with method + ›

lemma infer_e_d_weakening:
  fixes e::e
  assumes "Θ ; Φ ; B ; Γ ; Δ ⊨ e ==> τ" and "setD Δ ⊆ setD Δ'" and "wfD Θ B Γ Δ'" 
  shows   "Θ; Φ ; B ; Γ ; Δ' ⊨ e ==> τ"
  using assms by(nominal_induct τ avoiding: Δ' rule: infer_e.strong_induct,auto simp add:infer_e.intros)

lemma  wfG_x_fresh_in_v_simple:
  fixes x::x and v :: v
  assumes "Θ; B; Γ ⊨ v ==> τ" and "atom x ♯ Γ" 
  shows "atom x ♯ v"
  using wfV_x_fresh infer_v_wf assms by metis

lemma check_s_g_weakening:
  fixes v::v and s::s and cs::branch_s and x::x and c::c and b::b and Γ'::Γ and Θ::Θ and css::branch_list
  shows  "check_s Θ Φ B Γ Δ s t ==> toSet Γ ⊆ toSet Γ' ==> Θ ; B ⊨_wf Γ' ==> check_s Θ Φ B Γ' Δ s t"  and 
    "check_branch_s Θ Φ B Γ Δ tid cons const v cs t ==> toSet Γ ⊆ toSet Γ' ==> Θ ; B ⊨_wf Γ' ==> check_branch_s Θ Φ B Γ' Δ tid cons const v cs t" and
    "check_branch_list Θ Φ B Γ Δ tid dclist v css t ==> toSet Γ ⊆ toSet Γ' ==> Θ ; B ⊨_wf Γ' ==> check_branch_list Θ Φ B Γ' Δ tid dclist v css t"
proof(nominal_induct t and t and t avoiding: Γ'   rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_valI Θ B Γ Δ' Φ v τ' τ)
  then show ?case using Typing.check_valI infer_v_g_weakening wf_weakening subtype_weakening  by metis
next
  case (check_letI x Θ Φ B Γ Δ e τ z s b c)
  hence xf:"atom x ♯ Γ'"  by metis
  show ?case proof
    show "atom x ♯ (Θ, Φ, B, Γ', Δ, e, τ)" using check_letI using fresh_prod4 xf by metis
    show "Θ ; Φ ; B ; Γ' ; Δ ⊨ e ==> { z : b | c }" using infer_e_g_weakening check_letI by metis
    show "atom z ♯ (x, Θ, Φ, B, Γ', Δ, e, τ, s)" 
      by(unfold fresh_prodN,auto simp add: check_letI fresh_prodN) 
    have "toSet ((x, b, c[z::=V_var x]_v) #_\<Gamma> Γ) ⊆ toSet ((x, b, c[z::=V_var x]_v) #_\<Gamma> Γ')" using check_letI toSet.simps 
      by (metis Un_commute Un_empty_right Un_insert_right insert_mono)
    moreover hence "Θ ; B ⊨_wf ((x, b, c[z::=V_var x]_v) #_\<Gamma> Γ')" using check_letI wfG_cons_weakening check_s_wf by metis
    ultimately show "Θ ; Φ ; B ; (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ' ; Δ ⊨ s <== τ" using check_letI by metis
  qed
next
  case (check_let2I x Θ Φ B G Δ t s1 τ s2)
  show ?case proof
    show "atom x ♯ (Θ, Φ, B, Γ', Δ, t, s1, τ)" using check_let2I using fresh_prod4 by auto
    show "Θ ; Φ ; B ; Γ' ; Δ ⊨ s1 <== t" using check_let2I by metis
    have "toSet ((x, b_of t, c_of t x) #_\<Gamma> G) ⊆ toSet ((x, b_of t, c_of t x ) #_\<Gamma> Γ')" using check_let2I by auto
    moreover hence "Θ ; B ⊨_wf ((x, b_of t, c_of t x) #_\<Gamma> Γ')" using check_let2I wfG_cons_weakening check_s_wf by metis
    ultimately show "Θ ; Φ ; B ; (x, b_of t, c_of t x) #_\<Gamma> Γ' ; Δ ⊨ s2 <== τ" using check_let2I by metis
  qed
next
  case (check_branch_list_consI Θ Φ B Γ Δ tid dclist' v cs τ css dclist)
  thus ?case using Typing.check_branch_list_consI by metis
next
  case (check_branch_list_finalI Θ Φ B Γ Δ tid dclist' v cs τ dclist)
  thus ?case using Typing.check_branch_list_finalI by metis
next
  case (check_branch_s_branchI Θ B Γ Δ τ const x Φ tid cons v  s)
  show ?case proof
    show "Θ; B; Γ' ⊨_wf Δ " using  wf_weakening2(6) check_branch_s_branchI by metis
    show "⊨_wf Θ" using check_branch_s_branchI by auto
    show "Θ; B; Γ' ⊨_wf τ "  using check_branch_s_branchI wfT_weakening ‹wfG Θ B Γ'› by presburger

    show "Θ ; {||} ; GNil ⊨_wf const " using check_branch_s_branchI by auto
    show "atom x ♯ (Θ, Φ, B, Γ', Δ, tid, cons, const, v, τ)" using check_branch_s_branchI by auto
    have "toSet ((x, b_of const, CE_val v == CE_val(V_cons tid cons (V_var x)) AND c_of const x) #_\<Gamma> Γ) ⊆ toSet ((x, b_of const, CE_val v == CE_val (V_cons tid cons (V_var x)) AND c_of const x) #_\<Gamma> Γ')" 
      using check_branch_s_branchI by auto
    moreover hence "Θ ; B ⊨_wf ((x, b_of const, CE_val v == CE_val (V_cons tid cons (V_var x)) AND c_of const x ) #_\<Gamma> Γ')" 
      using check_branch_s_branchI wfG_cons_weakening check_s_wf by metis
    ultimately show "Θ ; Φ ; B ; (x, b_of const, CE_val v == CE_val (V_cons tid cons (V_var x)) AND c_of const x ) #_\<Gamma> Γ' ; Δ ⊨ s <== τ" 
      using check_branch_s_branchI  using fresh_dom_free by auto
  qed
next
  case (check_ifI z Θ Φ B Γ Δ v s1 s2 τ)
  show ?case proof
    show ‹atom z ♯ (Θ, Φ, B, Γ', Δ, v, s1, s2, τ)› using fresh_prodN check_ifI by auto
    show ‹Θ; B; Γ' ⊨ v <== { z : B_bool | TRUE }› using check_v_g_weakening check_ifI by auto
    show ‹ Θ ; Φ ; B ; Γ' ; Δ ⊨ s1 <== { z : b_of τ | CE_val v == CE_val (V_lit L_true) IMP c_of τ z }› using  check_ifI by auto
    show ‹ Θ ; Φ ; B ; Γ' ; Δ ⊨ 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_whileI Δ G P s1 z s2 τ')
  then show ?case using check_s_check_branch_s_check_branch_list.intros check_v_g_weakening subtype_weakening wf_weakening  
    by (meson infer_v_g_weakening)
next
  case (check_seqI Δ G P s1 z s2 τ)
  then show ?case using check_s_check_branch_s_check_branch_list.intros check_v_g_weakening subtype_weakening wf_weakening 
    by (meson infer_v_g_weakening)
next
  case (check_varI u Θ Φ B Γ Δ τ' v τ s)
  thus ?case  using check_v_g_weakening check_s_check_branch_s_check_branch_list.intros by auto
next
  case (check_assignI Θ Φ B Γ Δ u τ v z τ')
  show ?case proof 
    show ‹Θ ⊨_wf Φ › using check_assignI by auto
    show ‹Θ; B; Γ' ⊨_wf Δ› using check_assignI  wf_weakening by auto
    show ‹(u, τ) ∈ setD Δ› using check_assignI by auto
    show ‹Θ; B; Γ' ⊨ v <== τ› using check_assignI  check_v_g_weakening by auto
    show ‹Θ; B; Γ' ⊨ { z : B_unit | TRUE } < τ'› using  subtype_weakening check_assignI by auto
  qed
next
  case (check_caseI Δ Γ Θ dclist cs τ tid v z)

  then show ?case using check_s_check_branch_s_check_branch_list.intros check_v_g_weakening subtype_weakening wf_weakening
    by (meson infer_v_g_weakening)
next
  case (check_assertI x Θ Φ B Γ Δ c τ s)
  show ?case proof
    show ‹atom x ♯ (Θ, Φ, B, Γ', Δ, c, τ, s)› using check_assertI by auto

    have " Θ ; B ⊨_wf (x, B_bool, c) #_\<Gamma> Γ" using check_assertI check_s_wf by metis
    hence *:" Θ ; B ⊨_wf (x, B_bool, c) #_\<Gamma> Γ'"   using wfG_cons_weakening check_assertI by metis
    moreover have "toSet ((x, B_bool, c) #_\<Gamma> Γ) ⊆ toSet ((x, B_bool, c) #_\<Gamma> Γ')" using check_assertI by auto
    thus  ‹ Θ ; Φ ; B ; (x, B_bool, c) #_\Γ Γ' ; Δ ⊨ s <== τ› using check_assertI(11) [OF _ *] by auto

    show ‹Θ; B; Γ' ⊨ c › using check_assertI valid_weakening by metis
    show ‹ Θ; B; Γ' ⊨_wf Δ › using check_assertI wf_weakening by metis
  qed
qed

lemma  wfG_xa_fresh_in_v:
  fixes c::c and Γ::Γ and G::Γ and v::v and xa::x
  assumes "Θ; B; Γ ⊨ v ==> τ" and "G=( Γ'@ (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ)" and "atom xa ♯ G" and "Θ ; B ⊨_wf G"
  shows "atom xa ♯ v"
proof -
  have "Θ; B; Γ ⊨_wf v : b_of τ"  using infer_v_wf assms by metis
  hence "supp v ⊆ atom_dom Γ ∪ supp B" using wfV_supp by simp
  moreover have  "atom xa ∉ atom_dom G"  
    using assms wfG_atoms_supp_eq[OF assms(4)] fresh_def by metis
  ultimately show ?thesis using fresh_def
    using assms infer_v_wf wfG_atoms_supp_eq
      fresh_GCons  fresh_append_g subsetCE
    by (metis wfG_x_fresh_in_v_simple)
qed

lemma fresh_z_subst_g:
  fixes G::Γ
  assumes "atom z' ♯ (x,v)" and ‹atom z' ♯ G›
  shows "atom z' ♯ G[x::=v]_\<Gamma>_v"
proof - 
  have "atom z' ♯ v" using assms fresh_prod2 by auto
  thus ?thesis  using fresh_subst_gv assms by metis
qed

lemma  wfG_xa_fresh_in_subst_v:
  fixes c::c and v::v and x::x  and Γ::Γ and G::Γ and xa::x
  assumes "Θ; B; Γ ⊨ v ==> τ" and "G=( Γ'@ (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ)" and "atom xa ♯ G" and "Θ ; B ⊨_wf G"
  shows "atom xa ♯ (subst_gv G x v)"
proof -
  have "atom xa ♯ v" using wfG_xa_fresh_in_v assms by metis
  thus ?thesis using fresh_subst_gv assms by metis
qed

subsection ‹Weakening Immutable Variable Context›

declare check_s_check_branch_s_check_branch_list.intros[simp]
declare check_s_check_branch_s_check_branch_list.intros[intro]

lemma check_s_d_weakening:
  fixes s::s and v::v and cs::branch_s and css::branch_list
  shows  " Θ ; Φ ; B ; Γ ; Δ ⊨ s <== τ ==> setD Δ ⊆ setD Δ' ==> wfD Θ B Γ Δ' ==> Θ ; Φ ; B ; Γ ; Δ' ⊨ s <== τ" and 
    "check_branch_s Θ Φ B Γ Δ tid cons const v cs τ ==> setD Δ ⊆ setD Δ' ==> wfD Θ B Γ Δ' ==> check_branch_s Θ Φ B Γ Δ' tid cons const v cs τ" and 
    "check_branch_list Θ Φ B Γ Δ tid dclist v css τ ==> setD Δ ⊆ setD Δ' ==> wfD Θ B Γ Δ' ==> check_branch_list Θ Φ B Γ Δ' tid dclist v css τ"
proof(nominal_induct τ and τ and τ avoiding: Δ'   arbitrary: v rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_valI Θ B Γ Δ Φ v τ' τ)
  then show ?case using check_s_check_branch_s_check_branch_list.intros by blast
next
  case (check_letI x Θ Φ B Γ Δ e τ z s b c)
  show ?case proof
    show "atom x ♯ (Θ, Φ, B, Γ, Δ', e, τ)"  using check_letI by auto
    show "atom z ♯ (x, Θ, Φ, B, Γ, Δ', e, τ, s)" using check_letI by auto
    show "Θ ; Φ ; B ; Γ ; Δ' ⊨ e ==> { z : b | c }"  using check_letI infer_e_d_weakening by auto
    have "Θ ; B ⊨_wf (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ" using check_letI check_s_wf by metis
    moreover have "Θ; B; Γ ⊨_wf Δ'" using check_letI check_s_wf by metis
    ultimately have "Θ; B; (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ ⊨_wf Δ'"  using wf_weakening2(6)  toSet.simps by fast
    thus  "Θ ; Φ ; B ; (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ ; Δ' ⊨ s <== τ"   using check_letI by simp
  qed
next
  case (check_branch_s_branchI Θ B Γ Δ τ const x Φ tid cons v  s)
  moreover have "Θ ;B ⊨_wf (x, b_of const, CE_val v == CE_val (V_cons tid cons (V_var x)) AND c_of const x ) #_\<Gamma> Γ" 
    using check_s_wf[OF check_branch_s_branchI(16) ] by metis
  moreover hence " Θ ;B ; (x, b_of const, CE_val v == CE_val (V_cons tid cons (V_var x)) AND c_of const x ) #_\<Gamma> Γ ⊨_wf Δ'" 
    using wf_weakening2(6) check_branch_s_branchI by fastforce
  ultimately show ?case 
    using  check_s_check_branch_s_check_branch_list.intros by simp
next
  case (check_branch_list_consI Θ Φ B Γ Δ tid dclist v cs τ css)
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_branch_list_finalI Θ Φ B Γ Δ tid dclist v cs τ)
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_ifI z Θ Φ B Γ Δ v s1 s2 τ)
  show ?case proof
    show ‹atom z ♯ (Θ, Φ, B, Γ, Δ', v, s1, s2, τ)› using fresh_prodN check_ifI by auto
    show ‹Θ; B; Γ ⊨ v <== { z : B_bool | TRUE }› using  check_ifI by auto
    show ‹ Θ ; Φ ; B ; Γ ; Δ' ⊨ s1 <== { z : b_of τ | CE_val v == CE_val (V_lit L_true) IMP c_of τ z }› using  check_ifI by auto
    show ‹ Θ ; Φ ; B ; Γ ; Δ' ⊨ 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_assertI x Θ Φ B Γ Δ c τ s)
  show ?case proof
    show "atom x ♯ (Θ, Φ, B, Γ, Δ', c, τ,s)" using fresh_prodN check_assertI by auto
    show *:" Θ; B; Γ ⊨_wf Δ' " using check_assertI by auto
    hence  "Θ; B; (x, B_bool, c) #_\<Gamma> Γ ⊨_wf Δ' " using wf_weakening2(6)[OF *, of " (x, B_bool, c) #_\<Gamma> Γ"] check_assertI check_s_wf toSet.simps by auto
    thus  "Θ ; Φ ; B ; (x, B_bool, c) #_\<Gamma> Γ ; Δ' ⊨ s <== τ" 
      using check_assertI(11)[OF ‹setD Δ ⊆ setD Δ'›] by simp
        (* wf_weakening2(6) check_s_wf check_assertI *)
    show "Θ; B; Γ ⊨ c " using fresh_prodN check_assertI by auto

  qed
next
  case (check_let2I x Θ Φ B G Δ t s1 τ s2)
  show ?case proof
    show "atom x ♯ (Θ, Φ, B, G, Δ', t , s1, τ)"  using check_let2I by auto

    show "Θ ; Φ ; B ; G ; Δ' ⊨ s1 <== t"  using check_let2I infer_e_d_weakening by auto
    have "Θ; B; (x, b_of t, c_of t x ) #_\<Gamma> G ⊨_wf Δ'"  using check_let2I wf_weakening2(6) check_s_wf by fastforce 
    thus  "Θ ; Φ ; B ; (x, b_of t, c_of t x) #_\<Gamma> G ; Δ' ⊨ s2 <== τ"   using check_let2I by simp
  qed
next
  case (check_varI u Θ Φ B Γ Δ τ' v τ s)
  show ?case proof
    show "atom u ♯ (Θ, Φ, B, Γ, Δ', τ', v, τ)" using check_varI by auto
    show "Θ; B; Γ ⊨ v <== τ'" using check_varI by auto
    have "setD ((u, τ') #_\<Delta>Δ) ⊆ setD ((u, τ') #_\<Delta>Δ')" using setD.simps check_varI by auto
    moreover have "u ∉ fst ` setD Δ'" using check_varI(1) setD.simps fresh_DCons   by (simp add: fresh_d_not_in)
    moreover hence "Θ; B; Γ ⊨_wf (u, τ') #_\<Delta>Δ' " using wfD_cons  fresh_DCons setD.simps check_varI check_v_wf  by metis
    ultimately show   "Θ ; Φ ; B ; Γ ; (u, τ') #_\<Delta>Δ' ⊨ s <== τ" using check_varI by auto
  qed
next
  case (check_assignI Θ Φ B Γ Δ u τ v z τ')
  moreover hence "(u, τ) ∈ setD Δ'" by auto
  ultimately show ?case using Typing.check_assignI by simp
next
  case (check_whileI Θ Φ B Γ Δ s1 z s2 τ')
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_seqI Θ Φ B Γ Δ s1 z s2 τ)
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_caseI Θ Φ B Γ Δ tid dclist v cs τ z)
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson

qed

lemma valid_ce_eq:
  fixes v::v and ce2::ce
  assumes "ce1 = ce2[x::=v]_cev" and "wfV Θ B GNil v b" and  "wfCE Θ B ((x, b, TRUE) #_\<Gamma> GNil) ce2 b'" and "wfCE Θ B GNil ce1 b'"
  shows ‹Θ; B; (x, b, ([[x ]^v]^ce == [ v ]^ce )) #_\Γ GNil ⊨ ce1 == ce2 ›
  unfolding valid.simps proof
  have wfg: "Θ ; B ⊨_wf (x, b, [ [ x ]^v ]^ce == [ v ]^ce ) #_\<Gamma> GNil" 
    using wfG_cons1I wfG_nilI wfX_wfY assms wf_intros 
    by (meson fresh_GNil wfC_e_eq wfG_intros2)

  show wf: ‹Θ; B; (x, b, [ [ x ]^v ]^ce == [ v ]^ce ) #_\Γ GNil ⊨_wf ce1 == ce2 ›
    apply(rule wfC_eqI[where b=b'])
    using wfg toSet.simps assms wfCE_weakening apply simp

    using wfg_ce_inside1de1 ssms
    using wfC_trueI wf_trans(8)  by auto

  show java.lang.NullPointerException
 ( \(ce1 == ce2 )))›
    fix i
    ume ; (x, b, [ [ x ]^cc\<Gamma> GNil ⊨ (x, b, [ [ x ]^c<up[v ^e ) #<^>\
    have 1:"wfV Θ[ \^v ]^e == [ v ]^e ) # GNil) v b" 
      using wf_weakening assms append_g.simps toSetwf
      by (metis empty_subsetI
    hence "∃ v \rbrakk "ng_xist] byo
    then obtain :lbrakk v ]

    hence ixme-
      have "i ⊨v ]^e == [ v ]^c_smps as b auto
      hence "i [[x]<supc⁼  [v]<^sup^e ] ~ True" using is_sat Ψ'"
      hence "i [v ]^\sup> ]sing
          iv eval_e_elims
        by (metis eval_c_elims(7) eval_e_uni eval_e_vl)
      ?i sin va__lims2eal_e_eims(1 bymei
    qed

    have 1:"wfCE Θ ((x, b, x]^supv ]^e  ==  [ v ]^e ) # Niljava.lang.StringIndexOutOfBoundsException: Index 134 out of bounds for length 134
      using wfCE_weakening assmsnd_gsfwfX_wfY
      by (metisempty_subsetI
    hence "∃ by(ule_a =(<>, φ)" in expandTauFrame) auto
    theninsertAssertion<>turnstilejava.lang.NullPointerException

    moreover have>⊗P' ⊨" using ‹ Ψ Ψ\<^ubbrshw "isetAsertion (extractFrame P') \<Psi<F φ"
      have show Ψ Ψ' ⊳
      moreover have ce1c2[:=]<sbc\sub>e\^>" using subst_v_ce_def assms subst_v_simple_commute by auto
 ultimately have "i(x ↦ ~ s1"
 using ix subst_e_eval_[oic11"e[z::= \^sup>v]]_v" x v s]iv s1y autoo
 "i(x \<mapsto ) = i" using ix by auto
 ultimately show ?thesis by auto
 qed
 ultimately show "i by(rl eatc.ae
 qed
 


  chec__t
 fixes v::v
 assumes "Θturstile> v <== τc_\^sub>v" and "Θ; B; GNil ⊨_wf { z : b_of τ | ce1 == ce2 }"
 and "supp ce1 ⊆ ⊗Q) ⊗' ⊳M( ≺
 shows "Θ; B; GNil ⊨ v <== {ttqrnsto opstionAscaiiyCommtaivitAsrtioSaETas
  -
 hereeet \Theta; B<urnstile 
 using assms chc_v_lims by metis

 then obtain z' and b' where *:"t = {v ]^cce \<rbrace  atom z' ♯ (Θ, B,GNil)"
 using assms infer_v_form by metis
 havevebq b_ft= _f\tau using subtype_eq_base2 b_of.simps t by auto
 obtain x::x where xf: ‹v ]^e == [ v ]^e , z, ce1 == ce2 )›
 using ave "(\Psi ⊗Q) ⊗' \rhd P ⟼M(xvcrpar⟨N⟩ ≺ P'" by(rule cComm2)

 have <><Γ_f (ce1[z::=[ x ]^v == ce2[z::=[ x ]^v )"
 using wfT_wfC2[OF assms(3), of x] subst_cv.simps(6) subst_v_c_def subst_v_ce_def fresh_GNil by simp

 then obtain b2 where b2: "Θ; Bbof t, TE) \^>\Gamma GNil ⊨w_v]
 Θ; BΓ GNil ⊨w_v] b" usn wf_elims()
 beq by metis

 from xf have "Θ; GNil 🚫e == [ \sup>c } { z : b_of t | ce1 = 2\rbrace"
 proof
 show ‹_f\<brace  [v]^<rbrace> <lose 
 w <> w z : b_of t | ce1 == ce2 } using beq assms by auto
 have ‹v ]^e == [ v ] GNil ⊨v]_supv]_v ) ›
 proof(rule valid_ce_eq)
 show ‹>v = ce2[z::=[ x ]^]_cv\closero -
 have "atom z ♯ ce1" using assms fresh_def thus ?case using \ <openguarded P›ag
 hence "ce1[z::=[ x ]^v]_v = ce1"
 using forget_subst_v by auto
 also have "... = ce2[z::=v]_cev" using assms by auto
 also have "... = ce2[z::=[ x ]^v]_v[x::=v]_cev" proof -
 have "atom x ♯ ce2" using xf fresh_prodN c.fresh by metis
 thus ?thesis using subst_v_simple_commute subst_v_ce_def by simp
 qed
 finally show ?thesis by auto
 qed
 show ‹ Θ; B; GNil ⊨_wf v : b_of t › using infer_v_wf t by simp
 show ‹ Θ; B; (x, b_of t, TRUE) #_\Γ GNil ⊨_wf ce2[z::=[ x ]^v]_v : b2 › using b2 by auto

 have " Θ; B; (x, b_of t, TRUE) #_\Γ GNil ⊨_wf ce1[z::=[ x ]^v]_v : b2" using b2 by auto
 moreover have "atom x ♯ ce1[z::=[ x ]^v]_v"
 using fresh_subst_v_if assms fresh_def
 using ‹Θ; B; GNil ⊨_wf v : b_of t› ‹ce1[z::=[ x ]^v]_v = ce2[z::=[ x ]^v]_v[x::=v]_cev›
 fresh_GNil subst_v_ce_def wfV_x_fresh by auto
 ultimately show ‹ Θ; B; GNil ⊨_wf ce1[z::=[ x ]^v]_v : b2 › using
 wf_restrict(8) by force
 qed
 moreover have v: "v[z'::=[ x ]^v]_vv = v"
 using forget_subst assms infer_v_wf wfV_supp x_not_in_b_set
 by (simp add: "local.*")
 ultimately show "Θ; B; (x, b_of t, ([ [ z' ]^v ]^ce == [ v ]^ce )[z'::=[ x ]^v]_v) #_\Γ GNil ⊨ (ce1 == ce2 )[z::=[ x ]^v]_v"
 unfolding subst_cv.simps subst_v_c_def subst_cev.simps subst_vv.simps
 using subst_v_ce_def by simp
 qed
 thus ?thesis using b_of.simps assms * check_v_subtypeI t b_of.simps subtype_eq_base2 by metis