Theory TypingL

(*<*)
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 Θ ℬ Γ (⦃ z : b_of t  | CE_val v  ==  CE_val (V_lit L_false) IMP  c_of t z  ⦄)" and "atom z ♯ (Γ,t)"
  shows "wfT Θ ℬ Γ 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 ‹ Θ; ℬ; Γ   ⊢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) #Γ Γ"
  shows "atom bv ♯ Γ' @ (x, b, TRUE) #Γ Γ"
  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  "Θ; ℬ; G ⊢wf v : b' ⟹ G =  Γ' @ (x, b, c) #Γ Γ ⟹ Θ ;  ℬ ;  Γ' @ ((x, b, TRUE) #Γ Γ) ⊢wf v : b'" and
  "Θ; ℬ; G  ⊢wf c'' ⟹  G =   Γ' @(x, b, c) #Γ Γ ⟹  Θ ;  ℬ ; Γ' @ ((x, b, TRUE) #Γ Γ) ⊢wf  c''" and
  "Θ ; ℬ ⊢wf G ⟹  G =   Γ' @(x, b, c) #Γ Γ ⟹    Θ ; ℬ ⊢wf   Γ' @ ((x, b, TRUE) #Γ Γ) " and
  "Θ; ℬ; G ⊢wf τ ⟹  G =   Γ' @(x, b, c) #Γ Γ ⟹  Θ ;  ℬ ;  Γ' @ ((x, b, TRUE) #Γ Γ) ⊢wf  τ" and
  "Θ; ℬ; Γ  ⊢wf ts ⟹  True" and 
  "⊢wf P ⟹ True" and
  "Θ ; ℬ ⊢wf b ⟹ True" and
  "Θ ;  ℬ ; G  ⊢wf ce : b' ⟹  G =   Γ' @(x, b, c) #Γ Γ ⟹  Θ ;  ℬ ;  Γ' @ ((x, b, TRUE) #Γ Γ) ⊢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 Θ ℬ)
  then show ?case using wf_intros by metis
next
  case (wfB_boolI Θ ℬ)
  then show ?case using wf_intros by metis
next
  case (wfB_unitI Θ ℬ)
  then show ?case using wf_intros by metis
next
  case (wfB_bitvecI Θ ℬ)
  then show ?case using wf_intros by metis
next
  case (wfB_pairI Θ ℬ b1 b2)
  then show ?case using wf_intros by metis
next
  case (wfB_consI Θ s dclist ℬ)
  then show ?case using wf_intros by metis
next
  case (wfB_appI Θ b s bv dclist ℬ)
  then show ?case using wf_intros by metis
next
  case (wfV_varI Θ ℬ Γ'' b' c x')
  hence wfg: ‹ Θ ; ℬ  ⊢wf Γ' @ (x, b, TRUE) #Γ Γ › by auto
  show ?case proof(cases "x=x'")
    case True
    hence "Some (b, TRUE) = lookup (Γ' @ (x, b, TRUE) #Γ Γ) 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) #Γ Γ) 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 Θ ℬ Γ l)
  then show ?case using wf_intros using wf_intros by metis
next
  case (wfV_pairI Θ ℬ Γ v1 b1 v2 b2)
  then show ?case using wf_intros by metis
next
  case (wfV_consI s dclist Θ dc x b' c ℬ Γ v)
  then show ?case using wf_intros by metis
next
  case (wfV_conspI s bv dclist Θ dc xc bc cc ℬ 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 ‹ Θ ;ℬ  ⊢wf b' ›  using wfV_conspI by metis
    show ‹ Θ; ℬ; Γ' @ (x, b, TRUE) #Γ Γ ⊢wf v : bc[bv::=b']bb ›  using wfV_conspI by metis
    have "atom bv ♯ Γ' @ (x, b, TRUE) #Γ Γ" using fresh_u_replace_true wfV_conspI by metis
    thus  ‹atom bv ♯ (Θ, ℬ, Γ' @ (x, b, TRUE) #Γ Γ, b', v)›  using wfV_conspI fresh_prodN by metis
  qed
next
  case (wfCE_valI Θ ℬ Γ v b)
  then show ?case using wf_intros by metis
next
  case (wfCE_plusI Θ ℬ Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_leqI Θ ℬ Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_eqI Θ ℬ Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_fstI Θ ℬ Γ v1 b1 b2)
  then show ?case using wf_intros by metis
next
  case (wfCE_sndI Θ ℬ Γ v1 b1 b2)
  then show ?case using wf_intros by metis
next
  case (wfCE_concatI Θ ℬ Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_lenI Θ ℬ Γ v1)
  then show ?case using wf_intros by metis
next
  case (wfTI z Θ ℬ Γ''  b' c')
  show ?case proof
    show ‹atom z ♯ (Θ, ℬ, Γ' @ (x, b, TRUE) #Γ Γ)›  using wfTI fresh_append_g fresh_GCons fresh_prodN  by auto
    show ‹ Θ ; ℬ  ⊢wf b' › using wfTI by metis
    show ‹ Θ; ℬ; (z, b', TRUE) #Γ Γ' @ (x, b, TRUE) #Γ Γ   ⊢wf c' ›  using wfTI append_g.simps by metis
  qed
next
  case (wfC_eqI Θ ℬ Γ e1 b e2)
  then show ?case using wf_intros by metis
next
  case (wfC_trueI Θ ℬ Γ)
  then show ?case using wf_intros by metis
next
  case (wfC_falseI Θ ℬ Γ)
  then show ?case using wf_intros by metis
next
  case (wfC_conjI Θ ℬ Γ c1 c2)
  then show ?case using wf_intros by metis
next
  case (wfC_disjI Θ ℬ Γ c1 c2)
  then show ?case using wf_intros by metis
next
  case (wfC_notI Θ ℬ Γ c1)
  then show ?case using wf_intros by metis
next
  case (wfC_impI Θ ℬ Γ c1 c2)
  then show ?case using wf_intros by metis
next
  case (wfG_nilI Θ ℬ)
  then show ?case  using GNil_append by blast
next
  case (wfG_cons1I c Θ ℬ Γ'' 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 Θ ℬ Γ'' 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 Θ ℬ Γ)
  then show ?case  using wf_intros by metis
next
  case (wfTs_cons Θ ℬ Γ τ 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   "Θ ; Φ ;  ℬ ; G ; D  ⊢wf e : b' ⟹ G =   Γ' @(x, b, c) #Γ Γ ⟹  Θ ; Φ ;  ℬ ;  Γ' @ ((x, b, TRUE) #Γ Γ); D ⊢wf e : b'" and
  "Θ ; Φ ; ℬ ; G ; Δ ⊢wf s : b' ⟹  G =   Γ' @(x, b, c) #Γ Γ ⟹ Θ ; Φ ; ℬ ;   Γ' @ ((x, b, TRUE) #Γ Γ) ; Δ ⊢wf s : b'" and
  "Θ ; Φ ; ℬ ; G ; Δ ; tid ; dc ; t ⊢wf cs : b' ⟹   G =   Γ' @(x, b, c) #Γ Γ ⟹ Θ ; Φ ; ℬ ;  Γ' @ ((x, b, TRUE) #Γ Γ) ; Δ ; tid ; dc ; t ⊢wf cs : b'" and
  "Θ ; Φ ; ℬ ; G ; Δ ; tid ; dclist ⊢wf css : b' ⟹   G =   Γ' @(x, b, c) #Γ Γ ⟹ Θ ; Φ ; ℬ ;   Γ' @ ((x, b, TRUE) #Γ Γ) ; Δ ; tid ; dclist ⊢wf css : b'" and

"Θ ⊢wf Φ ⟹ True" and
"Θ; ℬ; G  ⊢wf Δ ⟹  G =   Γ' @(x, b, c) #Γ Γ ⟹  Θ ;  ℬ ;  Γ' @ ((x, b, TRUE) #Γ Γ) ⊢wf Δ" and

"Θ ; Φ  ⊢wf ftq ⟹ True" and
"Θ ; Φ ; ℬ ⊢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 Θ Φ ℬ Γ Δ v b)
  then show ?case using wf_intros using wf_intros wf_replace_true1 by metis
next
  case (wfE_plusI Θ Φ ℬ Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_leqI Θ Φ ℬ Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_eqI Θ Φ ℬ Γ Δ v1 b v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_fstI Θ Φ ℬ Γ Δ v1 b1 b2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_sndI Θ Φ ℬ Γ Δ v1 b1 b2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_concatI Θ Φ ℬ Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_splitI Θ Φ ℬ Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_lenI Θ Φ ℬ Γ Δ v1)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_appI Θ Φ ℬ Γ Δ f x b c τ s v)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_appPI Θ Φ ℬ Γ'' Δ b' bv v τ f x1 b1 c1 s)
  show ?case proof
    show ‹ Θ  ⊢wf Φ › using wfE_appPI wf_replace_true1 by metis
    show ‹ Θ; ℬ; Γ' @ (x, b, TRUE) #Γ Γ ⊢wf Δ › using wfE_appPI by metis
    show ‹ Θ ; ℬ  ⊢wf b' › using wfE_appPI by metis
    have "atom bv ♯ Γ' @ (x, b, TRUE) #Γ Γ" using fresh_u_replace_true wfE_appPI fresh_prodN by metis
    thus  ‹atom bv ♯ (Φ, Θ, ℬ, Γ' @ (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 ‹ Θ; ℬ; Γ' @ (x, b, TRUE) #Γ Γ ⊢wf v : b1[bv::=b']b  › using wfE_appPI wf_replace_true1 by metis
  qed
next
  case (wfE_mvarI Θ Φ ℬ Γ Δ u τ)
  then show ?case using wf_intros wf_replace_true1 by metis
next

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

next
  case (wfS_assignI u τ Δ Θ ℬ Γ Φ v)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfS_whileI Θ Φ ℬ Γ Δ s1 s2 b)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfS_seqI Θ Φ ℬ Γ Δ s1 s2 b)
  then show ?case using wf_intros by metis
next
  case (wfS_matchI Θ ℬ Γ'' v tid dclist Δ Φ cs b')
  show ?case proof
    show ‹ Θ; ℬ; Γ' @ (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 ‹ Θ; ℬ; Γ' @ (x, b, TRUE) #Γ Γ ⊢wf Δ › using wfS_matchI by auto
    show ‹ Θ  ⊢wf Φ › using wfS_matchI by auto
    show ‹ Θ ; Φ ; ℬ ; Γ' @ (x, b, TRUE) #Γ Γ ; Δ ; tid ; dclist ⊢wf cs : b' › using wfS_matchI by auto
  qed
next
  case (wfS_branchI Θ Φ ℬ x' τ Γ'' Δ s b' tid dc)
  show ?case proof
    have ‹ Θ ; Φ ; ℬ ; ((x', b_of τ, TRUE) #Γ Γ') @ (x, b, TRUE) #Γ Γ ; Δ ⊢wf s : b' › using wfS_branchI append_g.simps by metis
    thus  ‹ Θ ; Φ ; ℬ ; (x', b_of τ, TRUE) #Γ Γ' @ (x, b, TRUE) #Γ Γ ; Δ ⊢wf s : b' › using wfS_branchI append_g.simps append_g.simps by metis
    show ‹atom x' ♯ (Φ, Θ, ℬ, Γ' @ (x, b, TRUE) #Γ Γ, Δ, Γ' @ (x, b, TRUE) #Γ Γ, τ)› using wfS_branchI by auto
    show ‹ Θ; ℬ; Γ' @ (x, b, TRUE) #Γ Γ ⊢wf Δ › using wfS_branchI by auto
  qed
next
  case (wfS_finalI Θ Φ ℬ Γ Δ tid dc t cs b)
  then show ?case using wf_intros by metis
next
  case (wfS_cons Θ Φ ℬ Γ Δ tid dc t cs b dclist css)
  then show ?case using wf_intros by metis
next
  case (wfD_emptyI Θ ℬ Γ)
  then show ?case  using wf_intros wf_replace_true1 by metis
next
  case (wfD_cons Θ ℬ Γ Δ τ 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  "Θ; ℬ; Γ ⊢wf  τ"
  shows "Θ; ℬ; Γ ⊢ τ ≲ τ"
proof -
  obtain z b c where *:"τ = ⦃ z : b  | c ⦄ ∧ atom z ♯ (Θ,ℬ,Γ) ∧  Θ; ℬ; (z, b, TRUE) #Γ Γ  ⊢wf c" 
    using  wfT_elims(1)[OF assms] by metis
  obtain x::x where **: "atom x ♯ (Θ, ℬ, Γ, c,  z ,c, z , c )" using obtain_fresh by metis
  have "Θ; ℬ; Γ ⊢ ⦃ z : b  | c ⦄ ≲ ⦃ z : b  | c ⦄" proof
    show "Θ; ℬ; Γ   ⊢wf ⦃ z : b  | c ⦄" using * assms by auto
    show "Θ; ℬ; Γ   ⊢wf ⦃ z : b  | c ⦄" using * assms by auto
    show "atom x ♯ (Θ, ℬ, Γ, z , c , z , c )" using fresh_prod6 fresh_prod5 ** by metis
    thus  "Θ; ℬ; (x, b, c[z::=V_var x]v) #Γ Γ  ⊨ 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: "Θ; ℬ;Γ ⊢wf (⦃ z1 : b | c1 ⦄)"
  shows "Θ; ℬ; Γ ⊢  (⦃ 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 "Θ; ℬ; Γ ⊢ t1 ≲ t2" 
  shows "Θ; ℬ; Γ ⊢wf t1 ∧ Θ; ℬ; Γ ⊢wf t2"
  using assms subtype_elims by metis

lemma  subtype_eq_base:
  assumes "Θ; ℬ; Γ ⊢  (⦃ z1 : b1| c1 ⦄)  ≲ (⦃ z2 : b2 | c2 ⦄)"
  shows "b1=b2"
  using subtype.simps  assms by auto

lemma subtype_eq_base2: 
  assumes "Θ; ℬ; Γ ⊢ t1  ≲ t2"
  shows "b_of t1 = b_of t2"
  using assms proof(rule  subtype.induct[of Θ  ℬ Γ 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 "Θ; ℬ; Γ ⊢  τ1  ≲  τ2" 
  shows "Θ; ℬ; Γ ⊢wf τ1 ∧Θ; ℬ; Γ ⊢wf τ2"
  using assms
proof(rule  subtype.induct[of Θ ℬ Γ τ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 "Θ; ℬ; Γ ⊢  τ1  ≲  τ2" 
  shows "Θ ; ℬ⊢wf Γ"
  using assms
proof(rule  subtype.induct[of Θ ℬ Γ τ1 τ2],goal_cases)
  case (1 Θ ℬ Γ 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 "Θ; ℬ; (z, b, c) #Γ Γ  ⊨ c'" and  "atom z ♯ Γ" and "atom x ♯ (z, c, z, c', Γ)"
  shows "Θ; ℬ; (x, b, (z ↔ x ) ∙ c) #Γ Γ  ⊨ (z ↔ x ) ∙ c'"
proof -
  have "(z ↔ x ) ∙ Θ; ℬ; (z ↔ x ) ∙ ((z, b,  c) #Γ Γ)  ⊨ (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 " Θ; ℬ; (z0,b,c0)#ΓG ⊨ c"   
  shows "wfG Θ ℬ G" and "wfC Θ ℬ ((z0,b,c0)#ΓG) c" and "atom z0 ♯ G"
  using valid.simps wfC_wf wfG_cons assms by metis+

lemma valid_wfT: 
  fixes z::x
  assumes " Θ; ℬ; (z0,b,c0[z::=V_var z0]v)#ΓG ⊨ c[z::=V_var z0]v" and "atom z0 ♯ (Θ, ℬ, G,c,c0)"
  shows "Θ; ℬ; G ⊢wf ⦃ z : b | c0 ⦄"    and  "Θ; ℬ; G ⊢wf ⦃ z : b | c ⦄"
proof -
  have "atom z0 ♯ c0" using assms fresh_Pair by auto
  moreover have *:" Θ ; ℬ ⊢wf (z0,b,c0[z::=V_var z0]cv)#ΓG" using valid_wf_all wfX_wfY assms subst_v_c_def by metis
  ultimately show wft: "Θ; ℬ; G ⊢wf ⦃ z : b | c0 ⦄"  using wfG_wfT[OF *] by auto

  have "atom z0 ♯ c" using assms fresh_Pair by auto
  moreover have wfc: "Θ; ℬ; (z0,b,c0[z::=V_var z0]v)#ΓG  ⊢wf c[z::=V_var z0]v" using valid_wf_all assms by metis
  have  "Θ; ℬ; G ⊢wf ⦃ z0 : b | c[z::=V_var z0]v ⦄" proof
    show ‹atom z0 ♯ (Θ, ℬ, G)› using assms fresh_prodN by simp
    show ‹ Θ ; ℬ  ⊢wf b › using wft wfT_wfB by force
    show ‹ Θ; ℬ; (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   "Θ; ℬ; G ⊢wf ⦃ z : b | c ⦄" by auto
qed

lemma valid_flip: 
  fixes c::c and z::x and z0::x and xx2::x
  assumes " Θ; ℬ; (xx2, b, c0[z0::=V_var xx2]v) #Γ Γ  ⊨ c[z::=V_var xx2]v" and 
    "atom xx2 ♯ (c0,Γ,c,z) " and "atom z0 ♯ (Γ,c,z)"
  shows " Θ; ℬ; (z0, b, c0) #Γ Γ  ⊨ c[z::=V_var z0]v"
proof -

  have " ⊢wf Θ" using assms valid_wf_all wfX_wfY by metis
  hence " Θ ;  ℬ ; (xx2 ↔ z0 ) ∙ ((xx2, b, c0[z0::=V_var xx2]v) #Γ Γ)  ⊨ ((xx2 ↔ z0 ) ∙ c[z::=V_var xx2]v)"
    using valid.eqvt True_eqvt assms beta_flip_eq theta_flip_eq by metis
  hence " Θ; ℬ; (((xx2 ↔ z0 ) ∙ xx2, b, (xx2 ↔ z0 ) ∙ c0[z0::=V_var xx2]v) #Γ (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 "Θ; ℬ; Γ ⊢ t1  ≲ t2" and "atom y ♯ Γ" and "t1 = ⦃ z1 : b  | c1 ⦄" and "t2 =  ⦃ z2 : b  | c2 ⦄"
  shows  "Θ; ℬ; ((y, b, c1[z1::=V_var y]v) #Γ Γ) ⊨ c2[z2::=V_var y]v"
  using assms proof(nominal_induct t2 avoiding: y rule: subtype.strong_induct)
  case (subtype_baseI x Θ ℬ Γ z c z' c' ba)

  hence "(x ↔ y) ∙ Θ ; (x ↔ y) ∙ ℬ ; (x ↔ y) ∙ ((x, ba, c[z::=[ x ]v]v) #Γ Γ)  ⊨ (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  "Θ; ℬ;  ((y, ba, (x ↔ y) ∙ c[z::=[ x ]v]v) #Γ Γ)  ⊨ (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 "Θ; ℬ; Γ ⊢ t1  ≲ t2" and "atom z ♯ Γ" and "t1 = ⦃ z : b  | c1 ⦄" and "t2 =  ⦃ z : b  | c2 ⦄"
  shows  "Θ; ℬ; ((z, b, c1) #Γ Γ) ⊨ 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 "Θ; ℬ; Γ ⊢ τ1 ≲ τ2" and "Θ; ℬ; Γ ⊢ τ2 ≲ τ3"
  shows "Θ; ℬ; Γ ⊢ τ1 ≲ τ3"
  using assms proof(nominal_induct  avoiding: τ3 rule: subtype.strong_induct)
  case (subtype_baseI x Θ ℬ Γ 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 "Θ; ℬ; Γ ⊢ ⦃ z : b  | c ⦄ ≲ ⦃ z'' : b | c''⦄" 
  proof(rule Typing.subtype_baseI)
    show ‹atom x ♯ (Θ, ℬ, Γ, z, c, z'', c'')› using t3 fresh_prodN subtype_baseI xf by simp
    show ‹ Θ; ℬ; Γ ⊢wf ⦃ z : b  | c ⦄ › using subtype_baseI by auto
    show ‹ Θ; ℬ; Γ ⊢wf ⦃ z'' : b  | c'' ⦄ › using subtype_baseI t3 subtype_elims by metis
    have " Θ; ℬ; (x, b, c'[z'::=[ x ]v]v) #Γ Γ  ⊨ c''[z''::=[ x ]v]v "
      using subtype_valid[OF ‹Θ; ℬ; Γ  ⊢ ⦃ z' : b  | c' ⦄ ≲ τ3› , of x z' b c' z'' c''] subtype_baseI 
        t3 by simp
    thus ‹Θ; ℬ; (x, b, c[z::=[ x ]v]v) #Γ Γ  ⊨ c''[z''::=[ x ]v]v ›
      using  valid_trans_full[of Θ ℬ 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 ℬ 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  ℬ Γ  e1 b" and "wfCE P  ℬ Γ  e2 b" 
  shows "P; ℬ; Γ ⊢ ⦃ z1 : b  | CE_val (V_var z1)  ==  e1 ⦄ ≲ (⦃ z2 : b  | CE_val (V_var z2)  ==  e2  ⦄)"
proof -

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

  have wst1: "wfT P ℬ Γ (⦃ 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 ℬ Γ (⦃ 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,  ℬ , z1, CE_val (V_var z1)  ==  e1 , z2, CE_val (V_var z2)  ==  e2 , Γ)" using obtain_fresh by blast
  moreover have vld: "P; ℬ ; (x, b, (CE_val (V_var z1)  ==  e1 )[z1::=V_var x]v) #Γ Γ  ⊨ (CE_val (V_var z2)  ==  e2 )[z2::=V_var x]v "  (is "P; ℬ ; ?G ⊨ ?c")
  proof -

    have wbg: "P; ℬ ⊢wf ?G  ∧ P ;  ℬ  ⊢wf Γ ∧  toSet Γ ⊆ toSet ?G"  proof -        
      have "P; ℬ ⊢wf ?G"  proof(rule wfG_consI) 
        show "P; ℬ ⊢wf Γ" using assms wfX_wfY by metis
        show "atom x ♯ Γ" using xf by auto
        show "P; ℬ  ⊢wf b " using assms(6) wfX_wfB by auto
        show "P; ℬ ; (x, b, TRUE) #Γ Γ   ⊢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; ℬ ⊢wf Γ" using wfG_elims by metis
      ultimately show ?thesis using toSet.simps by auto 
    qed

    have wsc: "wfC P ℬ ?G ?c" proof -
      have "wfCE P ℬ ?G  (CE_val (V_var x)) b" proof      
        show ‹ P; ℬ ; (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 ℬ ?G e2 b" using wf_weakening assms wbg by metis
      ultimately have "wfC P ℬ ?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 ℬ ?G e1 b ∧ wfCE  P ℬ ?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, ℬ, Γ,  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 ℬ 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  ℬ GNil  e1 b" and "wfCE  P  ℬ GNil  e2 b"  and "atom z1 ♯ GNil" and "atom z2 ♯ GNil"
  shows "P; ℬ ; 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 v1 = {}" and "supp (V_pair v1 v2) = {}" and "wfTh P" and "wfCE  P ℬ GNil (CE_val v1) b" and "wfCE  P ℬ GNil  (CE_fst [V_pair v1 v2]ce) b" and 
    "wfCE  P ℬ GNil  (CE_val v2) b2"  and "atom z1 ♯ GNil" and "atom z2 ♯ GNil"
  shows "P; ℬ ; GNil  ⊢ (⦃ z1 : b | CE_val (V_var z1)  ==  CE_val v1  ⦄) ≲ (⦃ z2 : b | CE_val (V_var z2)  ==  CE_fst [V_pair v1 v2]ce ⦄)"
proof - 
  have "∀i s1 s2 G . wfG P ℬ G ∧ wfI P G i ∧ eval_e i ( CE_val v1) s1 ∧ eval_e i  (CE_fst [V_pair v1 v2]ce) s2 ⟶ s1 = s2" proof(rule+) 
    fix i s1 s2 G
    assume as: "wfG P ℬ G ∧ wfI P G i ∧ eval_e i (CE_val v1) s1 ∧ eval_e i (CE_fst [V_pair v1 v2]ce) s2"
    hence "wfCE  P ℬ G  (CE_val v2) b2" using assms wf_weakening 
      by (metis empty_subsetI toSet.simps(1))
    then obtain s3 where "eval_e i (CE_val v2) s3" using wfI_wfCE_eval_e as by metis
    hence "eval_v i ((V_pair  v1 v2)) (SPair s1 s3)"
      by (meson as eval_e_elims(1) eval_v_pairI)
    hence "eval_e i (CE_fst [V_pair v1 v2]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 v1 v2]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 v2 = {}" and "supp (V_pair v1 v2) = {}" and "wfTh P" and "wfCE  P ℬ GNil  (CE_val v2) b" and 
    "wfCE  P ℬ GNil  (CE_snd [(V_pair v1 v2)]ce) b" and 
    "wfCE  P ℬ GNil  (CE_val v1) b2"  and "atom z1 ♯ GNil" and "atom z2 ♯ GNil"
  shows "P; ℬ ; GNil  ⊢ (⦃ z1 : b | CE_val (V_var z1)  ==  CE_val v2  ⦄) ≲ (⦃ z2 : b | CE_val (V_var z2)  ==  CE_snd [(V_pair v1 v2)]ce ⦄)"
proof - 
  have "∀i s1 s2 G. wfG P ℬ G ∧ wfI P G i ∧ eval_e i ( CE_val v2) s1 ∧ eval_e i  (CE_snd [(V_pair v1 v2)]ce) s2 ⟶ s1 = s2" proof(rule+) 
    fix i s1 s2 G
    assume as: " wfG P ℬ G ∧ wfI P G i ∧ eval_e i (CE_val v2) s1 ∧ eval_e i (CE_snd [(V_pair v1 v2)]ce) s2"
    hence "wfCE  P ℬ G  (CE_val v1) b2" using assms wf_weakening 
      by (metis empty_subsetI toSet.simps(1))
    then obtain s3 where "eval_e i (CE_val v1) s3" using wfI_wfCE_eval_e as by metis
    hence "eval_v i ((V_pair  v1 v2)) (SPair s3 s1)"
      by (meson as eval_e_elims eval_v_pairI)
    hence "eval_e i (CE_snd [(V_pair v1 v2)]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 v1 v2]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[[v1,v2]v]ce]ce : b" 
  shows "Θ ;  {||} ; GNil  ⊢ (⦃ z1 : b | [[z1]v]ce ==  [v1]ce  ⦄) ≲ 
        (⦃ z2 : b | [[z2]v]ce ==   [#1[[v1, v2]v]ce]ce ⦄)"
proof  -
  obtain b2 where **:" Θ ;   {||} ; GNil ⊢wf V_pair v1 v2 : 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 v1 : b1'  ∧  Θ ;   {||} ; GNil ⊢wf v2 : b2'" 
    using wfV_elims(3)[OF **] by metis

  show ?thesis proof(rule subtype_gnil_fst_aux)
    show ‹supp v1 = {}› using * wfV_supp_nil by auto
    show ‹supp (V_pair v1 v2) = {}› using ** wfV_supp_nil e.supp by metis
    show ‹⊢wf Θ› using assms wfX_wfY   by metis
    show ‹Θ; {||}; GNil  ⊢wf CE_val v1 : b › using  wfCE_valI  "*" by auto
    show ‹Θ; {||}; GNil  ⊢wf CE_fst [V_pair v1 v2]ce : b › using assms by auto
    show ‹Θ; {||}; GNil  ⊢wf CE_val v2 : b2 ›using  wfCE_valI  "*" by auto
    show ‹atom z1 ♯ GNil› using fresh_GNil by metis
    show ‹atom z2 ♯ GNil› using fresh_GNil by metis
  qed
qed

lemma subtype_gnil_snd:
  assumes "wfCE  P  {||} GNil  (CE_snd ([V_pair v1 v2]ce)) b" 
  shows "P ;  {||} ; GNil  ⊢ (⦃ z1 : b | CE_val (V_var z1)  ==  CE_val v2  ⦄) ≲ (⦃ z2 : b | CE_val (V_var z2)  ==  CE_snd [(V_pair v1 v2)]ce ⦄)"
proof  -
  obtain b1 where **:" P ;   {||} ; GNil ⊢wf V_pair v1 v2 : 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 v1 : b1'  ∧  P ;   {||} ; GNil ⊢wf v2 : b2'" using wfV_elims(3)[OF **] by metis

  show ?thesis proof(rule subtype_gnil_snd_aux)
    show ‹supp v2 = {}› using * wfV_supp_nil by auto
    show ‹supp (V_pair v1 v2) = {}› using ** wfV_supp_nil e.supp by metis
    show ‹⊢wf P› using assms wfX_wfY  by metis
    show ‹P; {||}; GNil  ⊢wf CE_val v1 : b1 › using wfCE_valI   "*" by simp
    show ‹P; {||}; GNil  ⊢wf CE_snd [(V_pair v1 v2)]ce : b › using assms by auto
    show ‹P; {||}; GNil  ⊢wf CE_val v2 : 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; ℬ; Γ ⊢ t1 ≲ t2"
  shows "atom x ♯ t2"
proof -
  have wfg: "P; ℬ ⊢wf  Γ" using subtype_wf wfX_wfY  assms by metis
  have wft: "wfT P ℬ Γ t2" using subtype_wf wfX_wfY assms by blast
  hence "supp t2 ⊆ atom_dom Γ ∪ supp ℬ" 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 ℬ GNil (⦃ z1 : b  | CE_val (V_lit l )  ==  CE_val (V_lit l)   IMP  c[z::=V_var z1]v  ⦄)" and
    "wfT P ℬ GNil (⦃ z : b  | c ⦄)" and "atom z1 ♯ c"
  shows  "P; ℬ ; 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 , ℬ , 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; ℬ ; (x, b, (CE_val (V_lit l)  ==  CE_val (V_lit l)   IMP  c[z::=V_var z1]v )[z1::=V_var x]v) #Γ GNil  ⊨ c[z::=V_var x]v " (is "P; ℬ ; ?G ⊨ ?c" ) proof -
    have "wfC P ℬ ?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, ℬ, 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; ℬ; Γ ⊢ ⦃ z : b  | c ⦄ ≲ ⦃ z' : b  | c' ⦄" and 
    "wfT P ℬ Γ (⦃ z1 : b  | CE_val v  ==  CE_val (V_lit l) IMP  c[z::=V_var z1]v  ⦄)"  and
    "wfT P ℬ Γ (⦃ 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; ℬ ; Γ ⊢ ⦃ 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,ℬ,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; ℬ ; (x, b, (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 z2]v )[z2::=V_var x]v" 
    (is "P; ℬ ; ?G ⊨ ?c" )
  proof -
    have wbc: "wfC P ℬ ?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 )) #Γ Γ)" using a1 is_satis_g.simps by meson
        moreover have "wfI P ((x,b,(c[z::=V_var x]v )) #Γ Γ) 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 ℬ ?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 ℬ ?G (c'[z'::=V_var z2]v[z2::=V_var x]v)" proof(rule wfT_wfC_cons)
          show ‹ P; ℬ; Γ ⊢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; ℬ; Γ ⊢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, ℬ, Γ, 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 "Θ; ℬ; GNil  ⊢wf e1 : b " and  "Θ; ℬ; GNil  ⊢wf e2 : b"
  shows    "Θ; ℬ; (x, b, (CE_val (V_var x)  ==  e1 )) #Γ  GNil  ⊨ (CE_val (V_var x)  ==  e2) "
proof(rule validI)
  show "Θ; ℬ; (x, b, CE_val (V_var x)  ==  e1 ) #Γ GNil  ⊢wf CE_val (V_var x)  ==  e2" 
  proof
    have " Θ ;  ℬ ; (x, b, TRUE )#Γ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 "Θ ; ℬ ⊢wf (x, b, CE_val (V_var x)  ==  e1 ) #Γ GNil" using wfG_consI fresh_GNil wfX_wfY assms wfX_wfB by metis
    thus "Θ; ℬ; (x, b, CE_val (V_var x)  ==  e1 ) #Γ GNil  ⊢wf CE_val (V_var x) : b " using  wfCE_valI wfV_varI wfX_wfY 
        lookup.simps  assms wfX_wfY by simp
    show "Θ; ℬ; (x, b, CE_val (V_var x)  ==  e1 ) #Γ GNil  ⊢wf e2 : b " using assms wf_weakening wfX_wfY 
      by (metis (full_types) ‹Θ; ℬ; (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 ) #Γ GNil) i ∧ is_satis_g i ((x, b, CE_val (V_var x)  ==  e1 ) #Γ 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 ) #Γ GNil) i ∧ is_satis_g i ((x, b, CE_val (V_var x)  ==  e1 ) #Γ 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 "Θ; ℬ; 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 "Θ; ℬ; GNil  ⊢ ?t1 ≲ ?t2")
proof -
  obtain x::x where x: "atom x ♯ (Θ, ℬ, 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: "Θ; ℬ; 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: "Θ; ℬ; 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 " Θ; ℬ; GNil  ⊢wf ?t1" using wfT_e_eq fresh_GNil wb1 wb2 by metis
    show " Θ; ℬ; GNil  ⊢wf ?t2" using wfT_e_eq fresh_GNil wb1 wb2 by metis
    show ?xfree using x by auto
    show "Θ; ℬ; (x, B_bitvec, (CE_val (V_var z)  ==  CE_val (V_lit (L_bitvec (v1 @ v2))) )[z::=V_var x]v) #Γ
           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 "Θ; ℬ; 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 "Θ; ℬ; GNil  ⊢ ?t1 ≲ ?t2")
proof -

  have *: "Θ  ⊢wf []  ∧  Θ; ℬ; GNil  ⊢wf []Δ " using assms wfG_nilI wfD_emptyI wfPhi_emptyI by auto
  obtain x::x where x: "atom x ♯  (Θ, ℬ, 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 "Θ  ; ℬ ; 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  "Θ; ℬ; GNil  ⊢wf  ?t1" using wfT_e_eq fresh_GNil by auto

    have "Θ  ; ℬ ; 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 "Θ; ℬ; GNil  ⊢wf  ?t2" using wfT_e_eq fresh_GNil  by auto

    show  "Θ; ℬ; (x, B_int, (CE_val (V_var z')  ==  CE_val (V_lit (L_num (int (length v)))) )[z'::=V_var x]v) #Γ GNil  ⊨ (CE_val (V_var z)  ==  CE_len [(V_lit (L_bitvec v))]ce )[z::=V_var x]v"
      (is "Θ; ℬ; ?G ⊨ ?c" ) using valid_len assms subst_v_c_def by auto      
  qed
qed

lemma subtype_base_fresh:
  assumes "Θ; ℬ; Γ ⊢wf ⦃ z : b  | c ⦄" and "Θ; ℬ; Γ ⊢wf ⦃ z : b  | c' ⦄ " and
    "atom z ♯ Γ" and "Θ; ℬ; (z, b, c) #Γ Γ  ⊨ c'"
  shows "Θ; ℬ; Γ ⊢ ⦃ z : b  | c ⦄ ≲ ⦃ z : b  | c' ⦄"
proof  -
  obtain x::x where *:"atom x ♯ ((Θ , ℬ , z, c, z, c', Γ) , (Θ, ℬ, Γ, ⦃ z : b  | c ⦄, ⦃ z : b  | c' ⦄))" using obtain_fresh by metis
  moreover hence "atom x ♯ Γ" using fresh_Pair by auto
  moreover hence "Θ; ℬ; (x, b, c[z::=V_var x]v) #Γ Γ  ⊨ 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 Θ ℬ  Γ" 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 "Θ; ℬ; Γ  ⊢ (⦃ 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 "Θ; ℬ; Γ  ⊢ ?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 "Θ; ℬ; Γ  ⊢ (⦃ 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 "Θ; ℬ; Γ  ⊢ ?S1 ≲ ?S2") 
  proof(rule  subtype_base_fresh)

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

    show  "wfT Θ ℬ Γ (⦃ x : b | CE_val (V_var x)  ==  CE_val (V_lit ll)  ⦄)" (is "wfT Θ ℬ ?A ?B") 
    proof(rule wfT_e_eq)
      have   " Θ; ℬ; Γ  ⊢wf (V_lit ll) : b" using wfV_litI base_for_lit.simps assms by metis
      thus " Θ; ℬ; Γ  ⊢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 Θ  ℬ  Γ (⦃ x : b  | CE_val (V_var x)  ==  CE_op opp [(V_lit (L_num n1))]ce [(V_lit (L_num n2))]ce  ⦄)" (is "wfT Θ ℬ  ?A ?C")
    proof(cases)
      case 1
      then show "Θ ; ℬ ; Γ   ⊢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 "Θ ; ℬ ; Γ   ⊢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   "Θ; ℬ ; (x, b, (CE_val (V_var x)  ==  CE_val (V_lit (ll)) )) #Γ Γ  
                          ⊨ (CE_val (V_var x)  ==  CE_op opp [V_lit (L_num n1)]ce [V_lit (L_num n2)]ce)" (is "Θ; ℬ; ?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 Θ ℬ  Γ" and "base_for_lit l1 = base_for_lit l2"
  shows "Θ; ℬ; Γ  ⊢ (⦃ 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 "Θ; ℬ; Γ  ⊢ ?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 , Γ, (Θ, ℬ, Γ))" 
    using obtain_fresh by blast

  have "Θ; ℬ; Γ  ⊢ (⦃ 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 "Θ; ℬ; Γ  ⊢ ?S1 ≲ ?S2") 
  proof(rule  subtype_base_fresh)

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

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

    show " Θ ; ℬ ; Γ   ⊢wf ⦃ x : B_bool  | [ [ x ]v ]ce  ==  [ eq [ [ l1 ]v ]ce [ [ l2 ]v ]ce ]ce  ⦄ "   
    proof(rule wfT_e_eq)
      show "Θ ; ℬ ; Γ ⊢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   "Θ; ℬ ; (x, B_bool, (CE_val (V_var x)  ==  CE_val (V_lit (?ll)) )) #Γ Γ  
                          ⊨ (CE_val (V_var x)  ==  CE_op Eq [V_lit (l1)]ce [V_lit (l2)]ce)" (is "Θ; ℬ; ?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 Θ ℬ G  (⦃ z : b | c  ⦄)"
  shows  "Θ; ℬ; G  ⊢  (⦃ z : b | c  ⦄) ≲ (⦃ z : b | TRUE  ⦄)"
proof - 
  obtain x::x where *: "atom x ♯ (Θ, ℬ, G,  z ,  c,  z , TRUE)" using obtain_fresh by blast
  then show ?thesis proof(rule subtype_baseI)
    show ‹ Θ; ℬ; G  ⊢wf ⦃ z : b  | c ⦄ › using assms by auto
    show ‹ Θ; ℬ;G  ⊢wf ⦃ z : b  | TRUE ⦄ › using wfT_TRUE assms wfX_wfY b_of.simps wfT_wf
      by (metis wfX_wfB(8))
    hence "Θ  ; ℬ  ⊢wf  (x, b, c[z::=V_var x]v) #Γ G" using wfT_wf_cons3 assms fresh_Pair * subst_v_c_def by auto
    thus  ‹Θ; ℬ; (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 "Θ ; ℬ ⊢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 ;  ℬ ; Γ ⊢ 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 Θ ℬ c x z)
  then show ?case using supp_at_base by auto
next
  case (infer_v_litI Θ ℬ Γ 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   "Θ ; ℬ  ⊢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 "Θ ; ℬ  ⊢wf Γ ∧ atom z ♯ Γ"
  shows  "Θ; ℬ; Γ ⊢wf  ⦃ z : base_for_lit l |  C_eq (CE_val (V_var z)) (CE_val (V_lit l)) ⦄"
proof 
  show "atom z ♯  (Θ, ℬ, Γ)" using  wfG_fresh_x assms by auto
  show "Θ ; ℬ  ⊢wf base_for_lit l" using base_for_lit_wf assms wfX_wfY by metis
  thus "Θ; ℬ; (z, base_for_lit l, TRUE) #Γ Γ   ⊢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 "Θ ; ℬ  ⊢wf Γ"
  shows "⊢wf Θ" and  "Θ ; ℬ   ⊢wf Γ" and "Θ; ℬ; Γ  ⊢wf τ"
proof -
  show *:"Θ ;  ℬ   ⊢wf Γ" using assms infer_l_elims by auto
  thus  "⊢wf Θ" using wfX_wfY by auto
  show *:"Θ ;  ℬ  ; Γ   ⊢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; ℬ ; 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 "Θ; ℬ; Γ ⊢ 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 ♯ (Θ, ℬ, Γ)"
  using infer_v_elims(1)[OF assms(1)] by metis

lemma infer_bool_options2:
  fixes v::v
  assumes "Θ; ℬ; Γ ⊢ 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 Θ ℬ Γ c x z)
  then show ?case using v.supp supp_at_base by auto
next
  case (infer_v_litI Θ ℬ Γ 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 "Θ; ℬ; Γ  ⊢ 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 "Θ; ℬ; Γ ⊢ 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 Θ ℬ Γ c x z)
  then show ?case using v.supp supp_at_base by auto
next
  case (infer_v_litI Θ ℬ Γ 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 "Θ; ℬ; Γ ⊢ 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 Θ ℬ Γ 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 Θ ℬ Γ 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 "Θ; ℬ; Γ ⊢ v ⇒ τ" 
  shows "∃z b. τ = (⦃ z : b | C_eq (CE_val (V_var z)) (CE_val v)⦄) ∧ atom z ♯ v ∧ atom z ♯ (Θ, ℬ, Γ)"
  using assms
proof(nominal_induct   rule: infer_v.strong_induct)
  case (infer_v_varI Θ ℬ Γ b c x z)
  then show ?case by force
next
  case (infer_v_litI Θ ℬ Γ l τ)
  then obtain z and b where "τ = ⦃ z : b  | CE_val (V_var z)  ==  CE_val (V_lit l)  ⦄ ∧atom z ♯ (Θ, ℬ, Γ) "
    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 Θ ℬ Γ t1 t2)
  then show ?case by force
next
  case (infer_v_consI s dclist Θ dc tc ℬ Γ 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 ℬ Γ 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 "Θ; ℬ; Γ ⊢ 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 "Θ; ℬ; Γ ⊢ v ⇒ τ"  and "atom z ♯ (v,Γ)"
  shows "Θ; ℬ; Γ ⊢ 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' ♯ (Θ, ℬ, Γ)" 
    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 "Θ; ℬ; Γ ⊢ v ⇒ τ"  and "atom z ♯ (v,Γ)" and "b = b_of τ"
  shows "Θ; ℬ; Γ ⊢ 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 "Θ; ℬ ; G ⊢ v ⇒ τ ⟹  Θ; ℬ; G ⊢wf v : (b_of τ)"
proof(induct rule: infer_v.induct)
  case (infer_v_varI Θ ℬ Γ b c x z)
  then show ?case using  wfC_elims  wf_intros by auto
next
  case (infer_v_pairI z v1 v2 Θ ℬ Γ t1 t2)
  then show ?case using  wfC_elims  wf_intros by auto
next
  case (infer_v_litI Θ ℬ Γ 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 ℬ Γ 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 ℬ Γ 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 ‹ Θ ; ℬ  ⊢wf b › using infer_v_conspI by auto
    show ‹atom bv ♯ (Θ, ℬ, Γ, 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 ‹ Θ; ℬ; Γ ⊢wf v : b1[bv::=b]bb › using infer_v_conspI by auto
  qed
qed

lemma infer_v_t_form_wf:
  assumes " wfB Θ ℬ b" and "wfV  Θ ℬ Γ v b" and "atom z ♯ Γ"
  shows "wfT Θ ℬ Γ ⦃ 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 "Θ; ℬ; G ⊢ v ⇒ τ"
  shows "wfT Θ ℬ G τ ∧  wfB  Θ ℬ (b_of τ) "
proof -
  obtain z and b where "τ = ⦃ z : b  | CE_val (V_var z)  ==  CE_val v  ⦄ ∧ atom z ♯ v ∧ atom z ♯ (Θ, ℬ, G)" using infer_v_form assms by metis
  moreover have  "wfB  Θ ℬ b" using infer_v_v_wf b_of.simps wfX_wfB(1) assms 
    using calculation by fastforce
  ultimately show "wfT Θ ℬ G τ ∧   wfB  Θ ℬ (b_of τ)" using infer_v_v_wf  infer_v_t_form_wf assms by fastforce
qed

lemma infer_v_wf: 
  fixes  v::v
  assumes "Θ; ℬ; G ⊢ v ⇒ τ"
  shows  "Θ; ℬ; G ⊢wf v : (b_of τ)" and "wfT Θ ℬ G τ"  and "wfTh Θ" and "wfG Θ ℬ G"
proof -
  show "Θ; ℬ; G ⊢wf v : b_of τ " using infer_v_v_wf assms by auto
  show "Θ; ℬ; G   ⊢wf τ" using infer_v_t_wf assms by auto
  thus  "Θ ; ℬ  ⊢wf G" using wfX_wfY by auto
  thus  "⊢wf Θ" using  wfX_wfY by auto
qed

lemma check_bool_options:
  assumes "Θ; ℬ; Γ  ⊢ v ⇐ ⦃ z : B_bool  | TRUE ⦄" and "supp v = {}"
  shows "v = V_lit L_true ∨ v = V_lit L_false"
proof -
  obtain t1 where  " Θ; ℬ; Γ  ⊢ t1 ≲  ⦃ z : B_bool  | TRUE ⦄ ∧ Θ; ℬ; Γ  ⊢ 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 "Θ; ℬ; Γ ⊢ v ⇐ τ"
  shows " Θ ; ℬ ⊢wf Γ" and "Θ; ℬ;Γ ⊢wf v : b_of τ" and "Θ; ℬ;Γ ⊢wf τ"
proof -
  obtain τ' where *: "Θ; ℬ; Γ ⊢ τ' ≲ τ ∧ Θ; ℬ; Γ ⊢ v ⇒ τ'" using check_v_elims assms by auto
  thus "Θ ; ℬ  ⊢wf Γ " and "Θ; ℬ;Γ ⊢wf v : b_of τ" and "Θ; ℬ; Γ ⊢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 "Θ; ℬ; Γ ⊢ 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 "Θ; ℬ; Γ ⊢ 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 ℬ Γ 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 ℬ Γ 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 ‹Θ; ℬ; Γ[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 Θ ℬ c x z)
  then show ?case using v.supp supp_at_base  by auto
next
  case (infer_v_litI Θ ℬ l)
  then show ?case by auto
next
  case (infer_v_consI dclist1 Θ dc tc ℬ Γ 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 Θ› ‹Θ; ℬ; Γ ⊢ 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 Θ ℬ Γ τ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 Θ ℬ Γ 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 ) #Γ Γ)  ⊨ ?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 "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ 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 "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ 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 "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ 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 "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ e ⇒ τ" 
  shows "Θ ; Φ ; ℬ ; Γ ; Δ ⊢wf e : b_of τ" 
  using assms proof(nominal_induct τ avoiding: τ rule: infer_e.strong_induct)
  case (infer_e_valI Θ ℬ Γ Δ' Φ v τ)
  then show ?case using  infer_v_v_wf wf_intros by metis
next
  case (infer_e_plusI Θ ℬ Γ Δ' Φ 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 Θ ℬ Γ Δ' 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 Θ ℬ Γ Δ' 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 Θ ℬ Γ Δ Φ f x b c τ' s' v τ'')
  have "Θ ; Φ ; ℬ ; Γ ; Δ ⊢wf AE_app f v : b_of τ' " proof 
    show ‹ Θ  ⊢wf Φ › using infer_e_appI by auto
    show ‹ Θ; ℬ; Γ ⊢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 "Θ; ℬ;Γ ⊢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' f bv x b c τ'' s' v τ')

  have "Θ ; Φ ; ℬ ; Γ ; Δ ⊢wf AE_appP f b' v : (b_of τ'')[bv::=b']b " proof
    show ‹ Θ  ⊢wf Φ › using infer_e_appPI by auto
    show ‹ Θ; ℬ; Γ ⊢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 "Θ ; ℬ  ⊢wf b'" using infer_e_appPI by auto
    show "Θ; ℬ;Γ ⊢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', 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 Θ ℬ Γ Δ' Φ 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 Θ ℬ Γ Δ' Φ 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 Θ ℬ Γ Δ' Φ 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 Θ ℬ Γ Δ' Φ 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 Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 z3)
  have " Θ ; Φ ; ℬ ; Γ ; Δ ⊢wf AE_split v1 v2  : B_pair B_bitvec B_bitvec"
  proof
    show "Θ  ⊢wf Φ" using infer_e_splitI by auto
    show "Θ; ℬ; Γ ⊢wf Δ" using infer_e_splitI by auto 
    show "Θ; ℬ; Γ ⊢wf v1 : B_bitvec" using infer_e_splitI b_of.simps infer_v_wf by metis
    show "Θ; ℬ; Γ ⊢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 "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ e ⇒ τ"
  shows "Θ; ℬ;Γ ⊢wf τ ∧ Θ  ⊢wf Φ" 
  using assms proof(induct  rule: infer_e.induct)
  case (infer_e_valI Θ ℬ Γ Δ' Φ v τ)
  then show ?case using infer_v_t_wf by auto
next
  case (infer_e_plusI Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
  hence "Θ; ℬ; Γ  ⊢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 Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
  hence " Θ; ℬ; Γ  ⊢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 Θ ℬ Γ Δ Φ v1 z1 b c1 v2 z2 c2 z3)
  hence " Θ; ℬ; Γ  ⊢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 Θ ℬ Γ Δ Φ f x b c τ s' v τ')
  show ?case proof
    show "Θ  ⊢wf Φ" using infer_e_appI by auto
    show "Θ; ℬ; Γ   ⊢wf τ'" proof -
      have *:" Θ; ℬ; Γ ⊢wf v : b " using infer_e_appI check_v_wf(2) b_of.simps by metis
      moreover have *:"Θ; ℬ; (x, b, c) #Γ Γ  ⊢wf τ" proof(rule  wf_weakening1(4))
        show ‹ Θ; ℬ; (x,b,c)#ΓGNil  ⊢wf τ › using  wfPhi_f_simple_wfT wfD_wf infer_e_appI wb_b_weakening by fastforce
        have "Θ ;  ℬ ; Γ ⊢wf ⦃ x : b | c ⦄" using infer_e_appI check_v_wf(3) by auto
        thus  ‹ Θ ;  ℬ ⊢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) #Γ Γ)[x::=v]Γ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' f bv x b c τ' s' v τ)

  have "Θ; ℬ; ((x, b[bv::=b']bb, c[bv::=b']cb) #Γ Γ)[x::=v]Γv ⊢wf (τ'[bv::=b']b)[x::=v]τv" 
  proof(rule wf_subst(4))
    show ‹ Θ; ℬ; (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  ‹ Θ; ℬ; (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 "Θ; ℬ; Γ ⊢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  ‹ Θ ; ℬ ⊢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 ‹ Θ; ℬ; Γ ⊢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) #Γ Γ)[x::=v]Γv = Γ" using subst_gv.simps by auto
  ultimately show ?case using infer_e_appPI subst_v_τ_def by simp
next
  case (infer_e_fstI Θ ℬ Γ Δ Φ v z' b1 b2 c z)
  hence "Θ; ℬ; Γ  ⊢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 Θ ℬ Γ Δ Φ v z' b1 b2 c z)
  hence "Θ; ℬ; Γ  ⊢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 Θ ℬ Γ Δ Φ v z' c z)
  hence "Θ; ℬ; Γ  ⊢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 Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
  hence "Θ; ℬ; Γ ⊢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 Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 z3)

  hence wfg: " Θ ; ℬ ⊢wf (z3, [ B_bitvec , B_bitvec ]b, TRUE) #Γ Γ" 
    using infer_v_wf wfG_cons2I wfB_pairI wfB_bitvecI by simp
  have wfz: "Θ; ℬ; (z3, [ B_bitvec , B_bitvec ]b, TRUE) #Γ Γ ⊢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: "Θ; ℬ; (z3, [ B_bitvec , B_bitvec ]b, TRUE) #Γ Γ ⊢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: "Θ; ℬ; (z3, [ B_bitvec , B_bitvec ]b, TRUE) #Γ Γ ⊢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 "Θ; ℬ; Γ   ⊢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 ♯ (Θ, ℬ, Γ)" using infer_e_splitI wfTh_x_fresh wfX_wfY fresh_prod3 wfG_fresh_x by metis
    show "Θ ; ℬ  ⊢wf [ B_bitvec , B_bitvec ]b " using wfB_pairI wfB_bitvecI infer_e_splitI wfX_wfY by metis
    show "Θ; ℬ; (z3, [ B_bitvec , B_bitvec ]b, TRUE) #Γ
              Γ   ⊢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 "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ e ⇒ τ"
  shows "Θ; ℬ; Γ ⊢wf τ" and "Θ ; ℬ  ⊢wf Γ" and "Θ; ℬ; Γ ⊢wf Δ" and "Θ ⊢wf Φ" and "Θ ; Φ ; ℬ ; Γ ; Δ ⊢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 "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ 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 :: "Θ ⇒ Φ ⇒ ℬ ⇒ Γ ⇒ Δ ⇒ 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 "Θ; ℬ; Γ ⊢ (⦃ z : B_unit | TRUE ⦄) ≲ τ"  and "wfD Θ ℬ Γ Δ" and "wfPhi Θ Φ"
  shows  "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ AS_val (V_lit L_unit ) ⇐ τ" 
proof - 
  have "wfG Θ ℬ Γ" 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 *:"Θ; ℬ; Γ ⊢ 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 Θ ℬ Γ (⦃ 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  "Θ; ℬ; Γ ⊢ (⦃ 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 Θ Φ ℬ Γ Δ e τ z s b c)
  then have *:"wfT Θ ℬ ((x, b , c[z::=V_var x]v) #Γ Γ) τ" by force
  moreover have "atom x ♯ τ" using check_letI fresh_prodN by force
  ultimately have "Θ; ℬ;Γ ⊢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 Θ Φ ℬ Γ Δ c τ s)
  then have *:"wfT Θ ℬ ((x, B_bool , c) #Γ Γ) τ" by force
  moreover have "atom x ♯ τ" using check_assertI fresh_prodN by force
  ultimately have "Θ; ℬ;Γ ⊢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 Θ ℬ Γ Δ τ cons const x v Φ s tid)
  then show ?case using wfX_wfY by metis
next
  case (check_branch_list_consI Θ Φ ℬ Γ Δ tid dclist' v cs τ css )
  then show ?case using wfX_wfY by metis
next
  case (check_branch_list_finalI Θ Φ ℬ Γ Δ tid dclist' v cs τ )
  then show ?case using wfX_wfY by metis
next
  case (check_ifI z Θ Φ ℬ Γ Δ v s1 s2 τ)
  hence *:"wfT Θ  ℬ Γ (⦃ z : b_of τ  | CE_val v  ==  CE_val (V_lit L_false) IMP  c_of τ z  ⦄)" (is "wfT Θ  ℬ Γ ?tau") by auto
  hence "wfT Θ ℬ Γ τ" using wfT_wfT_if1 check_ifI  fresh_prodN by metis
  hence " Θ; ℬ; Γ   ⊢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 Θ Φ ℬ G Δ t s1 τ s2)
  then have "wfT Θ ℬ ((x, b_of t, (c_of t x)) #Γ G) τ" by fastforce
  moreover have "atom x ♯ τ" using check_let2I by force
  ultimately have "wfT Θ ℬ  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 Θ Φ ℬ Γ Δ 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 Θ ℬ Γ ⦃ 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 Θ Φ ℬ Γ Δ  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 Θ ℬ Γ Δ Φ 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 Θ Φ ℬ Γ Δ e τ z s b c)
  show ?case proof
    show ‹ Θ ; Φ ; ℬ ; Γ ; Δ ⊢wf e : b › using infer_e_wf check_letI b_of.simps by metis
    show ‹ Θ ; Φ ; ℬ ; (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 ‹ Θ; ℬ; Γ ⊢wf Δ ›  using infer_e_wf check_letI b_of.simps by metis
    show ‹atom x ♯ (Φ, Θ, ℬ, Γ, Δ, e, b_of τ)› 
      apply(simp add: fresh_prodN, intro conjI)
      using  check_letI(1) fresh_prod7 by simp+ 
  qed
next
  case (check_assertI x Θ Φ ℬ Γ Δ c τ s)
  show ?case proof

    show ‹ Θ ; Φ ; ℬ ; (x, B_bool, c) #Γ Γ ; Δ ⊢wf s : b_of τ › using check_assertI by auto
  next
    show ‹ Θ; ℬ; Γ   ⊢wf c › using check_assertI by auto
  next
    show ‹ Θ; ℬ; Γ ⊢wf Δ › using check_assertI by auto
  next
    show ‹atom x ♯ (Φ, Θ, ℬ, Γ, Δ, c, b_of τ, s)› using check_assertI by auto
  qed
next
  case (check_branch_s_branchI Θ ℬ Γ Δ τ const x Φ tid cons v s)
  show ?case proof
    show ‹ Θ ; Φ ; ℬ ; (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 ♯ (Φ, Θ, ℬ, Γ, Δ, Γ, const)› 
      using wf_replace_true append_g.simps check_branch_s_branchI fresh_prodN by metis
    show ‹ Θ; ℬ; Γ ⊢wf Δ › using wf_replace_true append_g.simps check_branch_s_branchI by metis
  qed
next
  case (check_branch_list_consI Θ Φ ℬ Γ Δ tid cons const v cs τ dclist css)
  then show ?case using wf_intros by metis
next
  case (check_branch_list_finalI Θ Φ ℬ Γ Δ tid cons const v cs τ)
  then show ?case using wf_intros by metis
next
  case (check_ifI z Θ Φ ℬ Γ Δ v s1 s2 τ)
  show ?case using wfS_ifI check_v_wf check_ifI b_of.simps by metis
next
  case (check_let2I x Θ Φ ℬ G Δ t s1 τ s2)
  show ?case proof
    show ‹ Θ ; Φ ; ℬ ; G ; Δ ⊢wf s1 : b_of t ›  using check_let2I  b_of.simps by metis 
    show ‹ Θ; ℬ; G   ⊢wf t ›  using  check_let2I check_s_check_branch_s_wf  by metis
    show ‹ Θ ; Φ ; ℬ ; (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 ♯ (Φ, Θ, ℬ, 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 Θ Φ ℬ Γ Δ τ' v τ s)
  show ?case proof
    show ‹ Θ; ℬ; Γ   ⊢wf τ' › using check_v_wf check_varI by metis
    show ‹ Θ; ℬ; Γ ⊢wf v : b_of τ' ›  using check_v_wf check_varI by metis
    show ‹atom u ♯ (Φ, Θ, ℬ, Γ, Δ, τ', v, b_of τ)›  using check_varI fresh_prodN u_fresh_b by metis
    show ‹ Θ ; Φ ; ℬ ; Γ ; (u, τ') #ΔΔ ⊢wf s : b_of τ ›  using check_varI by metis
  qed   
next
  case (check_assignI Θ Φ ℬ Γ Δ u τ v z τ')
  then show ?case using wf_intros check_v_wf subtype_eq_base2 b_of.simps by metis
next
  case (check_whileI Θ Φ ℬ Γ Δ 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 Θ Φ ℬ Γ Δ s1 z s2 τ)
  thus ?case using wf_intros  b_of.simps  by metis
next
  case (check_caseI Θ Φ ℬ Γ Δ tid dclist v cs τ z)
  show  ?case proof
    show ‹ Θ; ℬ; Γ ⊢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 ‹ Θ; ℬ; Γ ⊢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 ‹ Θ ; Φ ; ℬ ; Γ ; Δ ; 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  "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ s ⇐ τ"
  shows "Θ ; Φ ; ℬ ; Γ ; ( u ↔ u') ∙ Δ  ⊢ (u ↔ u') ∙ s ⇐  τ" 
proof - 
  have  "(u ↔ u') ∙ Θ ; (u ↔ u') ∙ Φ ;  (u ↔ u') ∙  ℬ ; (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 , τ') #ΔΔ  ⊢ s ⇐  τ"
  shows "Θ ; Φ ; B ; Γ ; ( u', τ' ) #ΔΔ ⊢ s' ⇐ τ"
proof -
  have "Θ ; Φ ; B ; Γ ; ( u' ↔ u) ∙ (( u , τ') #ΔΔ)  ⊢ ( u' ↔ u) ∙ s ⇐  τ"
    using assms check_s_flip_u by metis
  moreover have " ( u' ↔ u) ∙ (( u , τ') #Δ Δ) = ( u' , τ') #ΔΔ" proof -
    have " ( u' ↔ u) ∙ (( u , τ') #Δ Δ) = ((u' ↔ u) ∙ u, (u' ↔ u) ∙ τ') #Δ (u' ↔ u) ∙ Δ"  
      using  DCons_eqvt  Pair_eqvt by auto
    also have "... = ( u' , (u' ↔ u) ∙ τ') #Δ Δ" 
      using assms flip_fresh_fresh by auto
    also have "... = ( u' , τ') #Δ Δ" 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  v1::v and  v2::v
  assumes "Θ; ℬ; Γ ⊢ v1 ⇒ τ1" and "Θ; ℬ; Γ ⊢ v2 ⇒ τ2"
  shows "∃τ. Θ; ℬ; Γ ⊢ V_pair v1 v2 ⇒ τ ∧ b_of τ = B_pair (b_of τ1) (b_of τ2)"
proof - 
  obtain z1 and b1 and c1 and z2 and b2 and c2 where zbc: "τ1 = (⦃ z1 : b1 | c1 ⦄) ∧ τ2 = (⦃ z2 : b2 | c2 ⦄)"
    using τ.exhaust by meson
  obtain z::x where "atom z ♯ ( v1, v2,Θ, ℬ,Γ)" using obtain_fresh
    by blast
  hence "atom z ♯ ( v1, v2) ∧ atom z ♯ (Θ, ℬ,Γ)" using fresh_prodN by metis
  hence " Θ; ℬ; Γ ⊢ V_pair v1 v2 ⇒ ⦃ z : [ b_of τ1 , b_of τ2 ]b  | CE_val (V_var z)  ==  CE_val (V_pair v1 v2)  ⦄"  
    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 v1 v2)  ⦄)" by blast
  moreover hence "b_of τ = B_pair (b_of τ1) (b_of τ2)" using b_of.simps zbc by presburger
  ultimately show ?thesis using b_of.simps by metis
qed

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

lemma infer_v_pair2E:
  assumes "Θ; ℬ; Γ ⊢ V_pair v1 v2 ⇒ τ"
  shows "∃τ1 τ2 z . Θ; ℬ; Γ ⊢ v1 ⇒ τ1 ∧ Θ; ℬ; Γ ⊢ v2 ⇒ τ2 ∧ 
           τ = (⦃ z : B_pair (b_of τ1) (b_of τ2) | C_eq (CE_val (V_var z)) (CE_val (V_pair v1 v2)) ⦄) ∧ atom z ♯  (v1, v2)" 
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 v1 v2)  ⦄) ∧
        atom z ♯ (v1, v2) ∧  Θ; ℬ; Γ ⊢ v1 ⇒ t1 ∧  Θ; ℬ; Γ ⊢ v2 ⇒ 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 "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ AE_app f v ⇒ τ"
  shows "∃x b c s' τ'.  wfD  Θ ℬ Γ Δ ∧ Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ' s'))) = lookup_fun Φ f ∧  Θ ⊢wf Φ ∧
       Θ; ℬ; Γ ⊢ v ⇐ ⦃ x : b  | c ⦄ ∧ τ = τ'[x::=v]τv ∧ atom x ♯ (Θ, Φ, ℬ, Γ, Δ, v, τ)"
  using infer_e_elims(6)[OF assms] b_of.simps subst_defs by metis

lemma infer_e_appP2E:
  fixes Φ::Φ and Θ::Θ
  assumes "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ AE_appP f b v ⇒ τ"
  shows "∃bv x ba c s' τ'.  wfD  Θ ℬ Γ Δ ∧ Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x ba c τ' s'))) = lookup_fun Φ f ∧  Θ ⊢wf Φ ∧  Θ ; ℬ  ⊢wf b   ∧
      (Θ; ℬ; Γ ⊢ v ⇐ ⦃ x : ba[bv::=b]bb  | c[bv::=b]cb ⦄) ∧ (τ = τ'[bv::=b]τb[x::=v]τv) ∧ atom x ♯ Γ ∧ atom bv ♯ v"
proof -
  obtain bv x ba c s' τ' where *:"wfD  Θ ℬ Γ Δ ∧ Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x ba c τ' s'))) = lookup_fun Φ f ∧  Θ ⊢wf Φ ∧  Θ ; ℬ  ⊢wf b   ∧
      (Θ; ℬ; Γ ⊢ v ⇐ ⦃ x : ba[bv::=b]bb  | c[bv::=b]cb ⦄) ∧ (τ = τ'[bv::=b]τb[x::=v]τv) ∧ atom x ♯ Γ ∧ atom bv ♯ (Θ, Φ, ℬ, Γ, Δ, 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 "Θ; ℬ; Γ ⊢ τ1 ≲ τ2" and  "toSet Γ ⊆ toSet Γ'" and "Θ ; ℬ ⊢wf Γ'" 
  shows  "Θ; ℬ; Γ' ⊢ τ1 ≲ τ2"
  using assms proof(nominal_induct τ2 avoiding: Γ' rule: subtype.strong_induct)

  case (subtype_baseI x Θ ℬ Γ z c z' c' b)
  show ?case proof
    show *:"Θ; ℬ; Γ'   ⊢wf ⦃ z : b  | c ⦄" using wfT_weakening subtype_baseI by metis
    show "Θ; ℬ; Γ'   ⊢wf ⦃ z' : b  | c' ⦄" using wfT_weakening subtype_baseI by metis
    show "atom x ♯ (Θ, ℬ, Γ',  z ,  c ,  z' ,  c' )" using subtype_baseI fresh_Pair by metis
    have "toSet ((x, b, c[z::=V_var x]v) #Γ Γ) ⊆  toSet ((x, b, c[z::=V_var x]v) #Γ Γ')" using subtype_baseI toSet.simps by blast
    moreover have "Θ ; ℬ ⊢wf (x, b, c[z::=V_var x]v) #Γ Γ'" using wfT_wf_cons3[OF *, of x] subtype_baseI fresh_Pair subst_defs by metis
    ultimately show "Θ; ℬ; (x, b, c[z::=V_var x]v) #Γ Γ'  ⊨ 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 "Θ;  ℬ ; Γ ⊢ v ⇒ τ" and "toSet Γ ⊆ toSet Γ'" and "Θ  ; ℬ ⊢wf Γ'"
  shows   "Θ;  ℬ ; Γ' ⊢ v ⇒ τ"
  using assms proof(nominal_induct   avoiding: Γ'  rule: infer_v.strong_induct)
  case (infer_v_varI Θ ℬ Γ b c x' z)  
  show ?case proof
    show ‹ Θ ; ℬ  ⊢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 ♯ (Θ, ℬ, Γ')› using infer_v_varI by auto
  qed
next
  case (infer_v_litI Θ ℬ Γ l τ)
  then show ?case using infer_v.intros by simp
next
  case (infer_v_pairI z v1 v2 Θ ℬ Γ t1 t2)
  then show ?case using infer_v.intros by simp
next
  case (infer_v_consI s dclist Θ dc tc ℬ Γ v tv z)
  show ?case proof 
    show ‹AF_typedef s dclist ∈ set Θ› using infer_v_consI by auto
    show ‹(dc, tc) ∈ set dclist› using infer_v_consI by auto
    show ‹ Θ; ℬ; Γ' ⊢ v ⇒ tv› using infer_v_consI by auto
    show ‹Θ; ℬ; Γ'  ⊢ tv ≲ tc› using infer_v_consI subtype_weakening by auto
    show ‹atom z ♯ v› using infer_v_consI by auto
    show ‹atom z ♯ (Θ, ℬ, Γ')› using infer_v_consI by auto
  qed
next
  case (infer_v_conspI s bv dclist Θ dc tc ℬ Γ v tv b z)
  show ?case proof
    show ‹AF_typedef_poly s bv dclist ∈ set Θ› using infer_v_conspI by auto
    show ‹(dc, tc) ∈ set dclist› using infer_v_conspI by auto 
    show ‹ Θ; ℬ; Γ' ⊢ v ⇒ tv› using infer_v_conspI by auto
    show ‹Θ; ℬ; Γ'  ⊢ tv ≲ tc[bv::=b]τb› using infer_v_conspI subtype_weakening by auto
    show ‹atom z ♯ (Θ, ℬ, Γ', v, b)› using infer_v_conspI by auto
    show ‹atom bv ♯ (Θ, ℬ, Γ', v, b)› using infer_v_conspI by auto
    show ‹ Θ ; ℬ  ⊢wf b › using infer_v_conspI by auto
  qed
qed

lemma check_v_g_weakening:
  fixes e::e and Γ'::Γ
  assumes "Θ;  ℬ ; Γ ⊢ v ⇐ τ" and "toSet Γ ⊆ toSet Γ'" and "Θ ; ℬ ⊢wf Γ'" 
  shows   "Θ;  ℬ ; Γ' ⊢ 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 "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ e ⇒ τ" and "toSet Γ ⊆ toSet Γ'" and "Θ ;  ℬ  ⊢wf Γ'"
  shows   "Θ ; Φ ;  ℬ ; Γ'; Δ ⊢ e ⇒ τ"
  using assms proof(nominal_induct τ avoiding: Γ'  rule: infer_e.strong_induct)
  case (infer_e_valI Θ ℬ Γ Δ' Φ v τ)
  then show ?case using infer_v_g_weakening wf_weakening infer_e.intros by metis
next
  case (infer_e_plusI Θ  ℬ Γ Δ Φ 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 "Θ ; Φ ;  ℬ ; Γ' ; Δ  ⊢ AE_op Plus v1 v2 ⇒ ⦃ z' : B_int  | CE_val (V_var z')  ==  CE_op Plus  [v1]ce [v2]ce  ⦄" proof
    show ‹ Θ ;  ℬ ; Γ'  ⊢wf Δ › using wf_weakening infer_e_plusI by auto
    show ‹ Θ  ⊢wf Φ › using infer_e_plusI by auto
    show ‹ Θ ;  ℬ ; Γ'  ⊢ v1 ⇒ ⦃ z1 : B_int  | c1 ⦄› using infer_v_g_weakening infer_e_plusI by auto
    show ‹ Θ ;  ℬ ; Γ'  ⊢ 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 Θ ℬ Γ Δ Φ 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 "Θ ; Φ ;  ℬ ; Γ' ; Δ  ⊢ AE_op LEq v1 v2 ⇒ ⦃ z' : B_bool  | CE_val (V_var z')  ==  CE_op LEq  [v1]ce [v2]ce  ⦄" proof
    show ‹ Θ ;  ℬ ; Γ'  ⊢wf Δ › using wf_weakening infer_e_leqI by auto
    show ‹ Θ  ⊢wf Φ › using infer_e_leqI by auto
    show ‹ Θ ;  ℬ ; Γ'  ⊢ v1 ⇒ ⦃ z1 : B_int  | c1 ⦄› using infer_v_g_weakening infer_e_leqI by auto
    show ‹ Θ ;  ℬ ; Γ'  ⊢ 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 Θ ℬ Γ Δ Φ 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 "Θ ; Φ ;  ℬ ; Γ' ; Δ  ⊢ AE_op Eq v1 v2 ⇒ ⦃ z' : B_bool  | CE_val (V_var z')  ==  CE_op Eq  [v1]ce [v2]ce  ⦄" proof
    show ‹ Θ ;  ℬ ; Γ'  ⊢wf Δ › using wf_weakening infer_e_eqI by auto
    show ‹ Θ  ⊢wf Φ › using infer_e_eqI by auto
    show ‹ Θ ;  ℬ ; Γ'  ⊢ v1 ⇒ ⦃ z1 : bb  | c1 ⦄› using infer_v_g_weakening infer_e_eqI by auto
    show ‹ Θ ;  ℬ ; Γ'  ⊢ 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 Θ ℬ Γ Δ Φ f x b c τ' s' v τ)
  show ?case proof 
    show "Θ; ℬ; Γ' ⊢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 "Θ; ℬ; Γ'  ⊢ v ⇐ ⦃ x : b  | c ⦄"  using wf_weakening infer_e_appI check_v_g_weakening by auto
    show "atom x ♯ (Θ, Φ, ℬ, Γ', Δ, 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' f bv x b c τ' s' v τ)

  hence *:"Θ ; Φ ; ℬ ; Γ ; Δ ⊢ 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 ‹ Θ ;  ℬ ; Γ'  ⊢wf Δ › using wf_weakening infer_e_appPI by auto
    show ‹ Θ  ⊢wf Φ › using wf_weakening infer_e_appPI by auto
    show "Θ ; ℬ  ⊢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 "Θ; ℬ; Γ'  ⊢ 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']τb = (x' ↔ x) ∙ (τ'[bv::=b']τ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', v, τ)" using infer_e_appPI fresh_prodN by metis
  qed

next
  case (infer_e_fstI Θ  ℬ Γ Δ Φ 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 "Θ ; Φ ;  ℬ ; Γ' ; Δ  ⊢ AE_fst v ⇒ ⦃ z' : b1  | CE_val (V_var z')  ==  CE_fst [v]ce  ⦄" proof
    show ‹ Θ ;  ℬ ; Γ'  ⊢wf Δ › using wf_weakening infer_e_fstI by auto
    show ‹ Θ  ⊢wf Φ › using wf_weakening infer_e_fstI by auto
    show "Θ ;  ℬ ; Γ'  ⊢ 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 Θ  ℬ Γ Δ Φ 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 "Θ ; Φ ;  ℬ ; Γ' ; Δ  ⊢ AE_snd v ⇒ ⦃ z' : b2  | CE_val (V_var z')  ==  CE_snd [v]ce  ⦄" proof
    show ‹ Θ ;  ℬ ;Γ'  ⊢wf Δ › using wf_weakening infer_e_sndI by auto
    show ‹ Θ  ⊢wf Φ › using wf_weakening infer_e_sndI by auto
    show "Θ ;  ℬ ; Γ'  ⊢ 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 Θ  ℬ Γ Δ Φ 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 "Θ ; Φ ; ℬ ; Γ' ; Δ  ⊢ AE_len v ⇒ ⦃ z' : B_int  | CE_val (V_var z')  ==  CE_len [v]ce  ⦄" proof
    show ‹ Θ; ℬ; Γ' ⊢wf Δ › using wf_weakening infer_e_lenI by auto
    show ‹ Θ  ⊢wf Φ › using wf_weakening infer_e_lenI by auto
    show "Θ ;  ℬ ; Γ' ⊢ 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 Θ  ℬ Γ Δ Φ 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 "Θ ; Φ ;  ℬ ; Γ' ; Δ  ⊢ AE_concat v1 v2 ⇒ ⦃ z' : B_bitvec  | CE_val (V_var z')  ==  CE_concat [v1]ce [v2]ce  ⦄" proof
    show ‹ Θ; ℬ; Γ' ⊢wf Δ › using wf_weakening infer_e_concatI by auto
    show ‹ Θ  ⊢wf Φ › using wf_weakening infer_e_concatI by auto
    show "Θ ;  ℬ ; Γ' ⊢ v1 ⇒ ⦃ z1 : B_bitvec  |  c1 ⦄" using infer_v_g_weakening infer_e_concatI    by metis
    show "Θ ;  ℬ ; Γ' ⊢ 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 Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 z3)
  show ?case proof
    show "Θ; ℬ; Γ' ⊢wf Δ" using infer_e_splitI wf_weakening by auto
    show "Θ  ⊢wf Φ " using infer_e_splitI wf_weakening by auto
    show "Θ; ℬ; Γ' ⊢ v1 ⇒ ⦃ z1 : B_bitvec  | c1 ⦄" using infer_v_g_weakening infer_e_splitI by metis
    show "Θ; ℬ; Γ'  ⊢ 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 "Θ ; Φ ; ℬ ; Γ ; Δ ⊢ e ⇒ τ" and "setD Δ ⊆ setD Δ'" and "wfD Θ  ℬ Γ Δ'" 
  shows   "Θ; Φ ;  ℬ ; Γ ; Δ' ⊢ 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 "Θ; ℬ; Γ ⊢ 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 Θ Φ ℬ Γ Δ s  t ⟹ toSet Γ ⊆ toSet Γ' ⟹  Θ ; ℬ ⊢wf Γ' ⟹ check_s Θ Φ ℬ Γ' Δ  s   t"  and 
    "check_branch_s Θ Φ ℬ Γ Δ  tid cons const v cs t ⟹  toSet Γ ⊆ toSet Γ' ⟹  Θ ; ℬ ⊢wf Γ'  ⟹ check_branch_s Θ Φ ℬ Γ' Δ tid cons const v cs t" and
    "check_branch_list Θ Φ ℬ Γ Δ  tid dclist v css t ⟹  toSet Γ ⊆ toSet Γ' ⟹  Θ ; ℬ ⊢wf Γ'  ⟹ check_branch_list Θ Φ ℬ Γ' Δ 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 Θ ℬ Γ Δ' Φ v τ' τ)
  then show ?case using Typing.check_valI infer_v_g_weakening wf_weakening subtype_weakening  by metis
next
  case (check_letI x Θ Φ ℬ Γ Δ e τ z s b c)
  hence xf:"atom x ♯ Γ'"  by metis
  show ?case proof
    show "atom x ♯ (Θ, Φ, ℬ, Γ', Δ, e, τ)" using check_letI using fresh_prod4 xf by metis
    show "Θ ; Φ ; ℬ ; Γ' ; Δ  ⊢ e ⇒ ⦃ z : b  | c ⦄" using infer_e_g_weakening check_letI by metis
    show "atom z ♯ (x, Θ, Φ, ℬ, Γ', Δ, e, τ, s)" 
      by(unfold fresh_prodN,auto simp add: check_letI fresh_prodN) 
    have "toSet ((x, b, c[z::=V_var x]v) #Γ Γ) ⊆ toSet ((x, b, c[z::=V_var x]v) #Γ Γ')" using check_letI toSet.simps 
      by (metis Un_commute Un_empty_right Un_insert_right insert_mono)
    moreover hence "Θ ; ℬ  ⊢wf ((x, b, c[z::=V_var x]v) #Γ Γ')" using check_letI wfG_cons_weakening check_s_wf by metis
    ultimately show "Θ ; Φ ; ℬ ; (x, b, c[z::=V_var x]v) #Γ Γ' ; Δ  ⊢ s ⇐ τ" using check_letI by metis
  qed
next
  case (check_let2I x Θ Φ ℬ G Δ t s1 τ s2)
  show ?case proof
    show "atom x ♯ (Θ, Φ, ℬ, Γ', Δ, t, s1, τ)" using check_let2I using fresh_prod4 by auto
    show "Θ ; Φ ; ℬ ; Γ' ; Δ  ⊢ s1 ⇐ t" using check_let2I by metis
    have "toSet ((x, b_of t, c_of t x) #Γ G) ⊆ toSet ((x, b_of t, c_of t x ) #Γ Γ')" using check_let2I by auto
    moreover hence "Θ ; ℬ  ⊢wf ((x, b_of t, c_of t x) #Γ Γ')" using check_let2I wfG_cons_weakening check_s_wf by metis
    ultimately show "Θ ; Φ ; ℬ ; (x, b_of t, c_of t x) #Γ Γ' ; Δ  ⊢ s2 ⇐ τ" using check_let2I by metis
  qed
next
  case (check_branch_list_consI Θ Φ ℬ Γ Δ tid dclist' v cs τ css dclist)
  thus ?case using Typing.check_branch_list_consI by metis
next
  case (check_branch_list_finalI Θ Φ ℬ Γ Δ tid dclist' v cs τ dclist)
  thus ?case using Typing.check_branch_list_finalI by metis
next
  case (check_branch_s_branchI Θ ℬ Γ Δ τ const x Φ tid cons v  s)
  show ?case proof
    show "Θ; ℬ; Γ' ⊢wf Δ " using  wf_weakening2(6) check_branch_s_branchI by metis
    show "⊢wf Θ" using check_branch_s_branchI by auto
    show "Θ; ℬ; Γ'   ⊢wf τ "  using check_branch_s_branchI wfT_weakening ‹wfG  Θ ℬ Γ'› by presburger

    show "Θ ; {||} ; GNil ⊢wf const " using check_branch_s_branchI by auto
    show "atom x ♯ (Θ, Φ, ℬ, Γ', Δ, 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) #Γ Γ) ⊆ toSet ((x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x)) AND  c_of const x) #Γ Γ')" 
      using check_branch_s_branchI by auto
    moreover hence "Θ ; ℬ  ⊢wf ((x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x))   AND  c_of const x ) #Γ Γ')" 
      using check_branch_s_branchI wfG_cons_weakening check_s_wf by metis
    ultimately show "Θ ; Φ ; ℬ ; (x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x))   AND  c_of const x ) #Γ Γ' ; Δ  ⊢ s ⇐ τ" 
      using check_branch_s_branchI  using fresh_dom_free by auto
  qed
next
  case (check_ifI z Θ Φ ℬ Γ Δ v s1 s2 τ)
  show ?case proof
    show ‹atom z ♯ (Θ, Φ, ℬ, Γ', Δ, v, s1, s2, τ)› using fresh_prodN check_ifI by auto
    show ‹Θ; ℬ; Γ'  ⊢ v ⇐ ⦃ z : B_bool  | TRUE ⦄› using check_v_g_weakening check_ifI by auto
    show ‹ Θ ; Φ ; ℬ ; Γ' ; Δ  ⊢ s1 ⇐ ⦃ z : b_of τ  | CE_val v  ==  CE_val (V_lit L_true)   IMP  c_of τ z  ⦄› using  check_ifI by auto
    show ‹ Θ ; Φ ; ℬ ; Γ' ; Δ  ⊢ 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 Θ Φ ℬ Γ Δ τ' v τ s)
  thus ?case  using check_v_g_weakening check_s_check_branch_s_check_branch_list.intros by auto
next
  case (check_assignI Θ Φ ℬ Γ Δ u τ v z τ')
  show ?case proof 
    show ‹Θ  ⊢wf Φ › using check_assignI by auto
    show ‹Θ; ℬ;  Γ' ⊢wf Δ› using check_assignI  wf_weakening by auto
    show ‹(u, τ) ∈ setD Δ› using check_assignI by auto
    show ‹Θ; ℬ; Γ'  ⊢ v ⇐ τ› using check_assignI  check_v_g_weakening by auto
    show ‹Θ; ℬ; Γ'  ⊢ ⦃ 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 Θ Φ ℬ Γ Δ c τ s)
  show ?case proof
    show ‹atom x ♯ (Θ, Φ, ℬ, Γ', Δ, c, τ, s)› using check_assertI by auto

    have " Θ ; ℬ  ⊢wf  (x, B_bool, c) #Γ Γ" using check_assertI check_s_wf by metis
    hence *:" Θ ; ℬ  ⊢wf  (x, B_bool, c) #Γ Γ'"   using wfG_cons_weakening check_assertI by metis
    moreover have "toSet ((x, B_bool, c) #Γ Γ) ⊆ toSet ((x, B_bool, c) #Γ Γ')" using check_assertI by auto
    thus  ‹ Θ ; Φ ; ℬ ; (x, B_bool, c) #Γ Γ' ; Δ  ⊢ s ⇐ τ› using check_assertI(11) [OF _ *] by auto

    show ‹Θ; ℬ; Γ'  ⊨ c › using check_assertI valid_weakening by metis
    show ‹ Θ; ℬ; Γ' ⊢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 "Θ; ℬ; Γ ⊢ v ⇒ τ" and "G=( Γ'@ (x, b, c[z::=V_var x]v) #Γ Γ)" and "atom xa ♯ G" and "Θ ; ℬ ⊢wf G"
  shows "atom xa ♯ v"
proof -
  have "Θ; ℬ; Γ ⊢wf v : b_of τ"  using infer_v_wf assms by metis
  hence "supp v ⊆ atom_dom Γ  ∪ supp ℬ" 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]Γ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 "Θ; ℬ; Γ ⊢ v ⇒ τ" and "G=( Γ'@ (x, b, c[z::=V_var x]v) #Γ Γ)" and "atom xa ♯ G" and "Θ ; ℬ ⊢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  " Θ ; Φ ; ℬ ; Γ ; Δ ⊢ s ⇐ τ ⟹  setD Δ ⊆ setD Δ' ⟹  wfD  Θ ℬ Γ Δ' ⟹ Θ ; Φ ; ℬ ; Γ ; Δ' ⊢ s ⇐ τ" and 
    "check_branch_s Θ Φ ℬ Γ Δ tid cons const v cs τ ⟹  setD Δ ⊆ setD Δ' ⟹  wfD  Θ ℬ Γ Δ' ⟹ check_branch_s Θ Φ ℬ Γ Δ' tid cons const v cs τ" and 
    "check_branch_list Θ Φ ℬ Γ Δ tid dclist v css τ ⟹  setD Δ ⊆ setD Δ' ⟹  wfD  Θ ℬ Γ Δ' ⟹ check_branch_list Θ Φ ℬ Γ Δ' 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 Θ ℬ Γ Δ Φ v τ' τ)
  then show ?case using check_s_check_branch_s_check_branch_list.intros by blast
next
  case (check_letI x Θ Φ ℬ Γ Δ e τ z s b c)
  show ?case proof
    show "atom x ♯ (Θ, Φ, ℬ, Γ, Δ', e, τ)"  using check_letI by auto
    show "atom z ♯ (x, Θ, Φ, ℬ, Γ, Δ', e, τ, s)" using check_letI by auto
    show "Θ ; Φ ; ℬ ; Γ ; Δ'  ⊢ e ⇒ ⦃ z : b  | c ⦄"  using check_letI infer_e_d_weakening by auto
    have "Θ ; ℬ ⊢wf (x, b, c[z::=V_var x]v) #Γ Γ" using check_letI check_s_wf by metis
    moreover have "Θ; ℬ; Γ ⊢wf Δ'" using check_letI check_s_wf by metis
    ultimately have "Θ; ℬ; (x, b, c[z::=V_var x]v) #Γ Γ ⊢wf Δ'"  using wf_weakening2(6)  toSet.simps by fast
    thus  "Θ ; Φ ; ℬ ; (x, b, c[z::=V_var x]v) #Γ Γ ; Δ'  ⊢ s ⇐ τ"   using check_letI by simp
  qed
next
  case (check_branch_s_branchI Θ ℬ Γ Δ τ const x Φ tid cons v  s)
  moreover have "Θ ;ℬ ⊢wf (x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x))   AND  c_of const x ) #Γ Γ" 
    using check_s_wf[OF check_branch_s_branchI(16) ] by metis
  moreover hence " Θ ;ℬ ; (x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x))   AND  c_of const x ) #Γ Γ ⊢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 Θ Φ ℬ Γ Δ 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 Θ Φ ℬ Γ Δ tid dclist v cs τ)
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_ifI z Θ Φ ℬ Γ Δ v s1 s2 τ)
  show ?case proof
    show ‹atom z ♯ (Θ, Φ, ℬ, Γ, Δ', v, s1, s2, τ)› using fresh_prodN check_ifI by auto
    show ‹Θ; ℬ; Γ  ⊢ v ⇐ ⦃ z : B_bool  | TRUE ⦄› using  check_ifI by auto
    show ‹ Θ ; Φ ; ℬ ; Γ ; Δ'  ⊢ s1 ⇐ ⦃ z : b_of τ  | CE_val v  ==  CE_val (V_lit L_true)   IMP  c_of τ z  ⦄› using  check_ifI by auto
    show ‹ Θ ; Φ ; ℬ ; Γ ; Δ'  ⊢ 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 Θ Φ ℬ Γ Δ c τ s)
  show ?case proof
    show "atom x ♯ (Θ, Φ, ℬ, Γ, Δ', c, τ,s)" using fresh_prodN check_assertI by auto
    show *:" Θ; ℬ; Γ ⊢wf Δ' " using check_assertI by auto
    hence  "Θ; ℬ; (x, B_bool, c) #Γ Γ ⊢wf Δ' " using wf_weakening2(6)[OF *, of " (x, B_bool, c) #Γ Γ"] check_assertI check_s_wf toSet.simps by auto
    thus  "Θ ; Φ ; ℬ ; (x, B_bool, c) #Γ Γ ; Δ'  ⊢ s ⇐ τ" 
      using check_assertI(11)[OF ‹setD Δ ⊆ setD Δ'›] by simp
        (* wf_weakening2(6) check_s_wf check_assertI *)
    show "Θ; ℬ; Γ  ⊨ c " using fresh_prodN check_assertI by auto

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

    show "Θ ; Φ ; ℬ ; G ; Δ'  ⊢ s1 ⇐ t"  using check_let2I infer_e_d_weakening by auto
    have "Θ; ℬ; (x, b_of t, c_of t x ) #Γ G ⊢wf Δ'"  using check_let2I wf_weakening2(6) check_s_wf by fastforce 
    thus  "Θ ; Φ ; ℬ ; (x, b_of t, c_of t x) #Γ G ; Δ'  ⊢ s2 ⇐ τ"   using check_let2I by simp
  qed
next
  case (check_varI u Θ Φ ℬ Γ Δ τ' v τ s)
  show ?case proof
    show "atom u ♯ (Θ, Φ, ℬ, Γ, Δ', τ', v, τ)" using check_varI by auto
    show "Θ; ℬ; Γ  ⊢ v ⇐ τ'" using check_varI by auto
    have "setD ((u, τ') #ΔΔ) ⊆ setD ((u, τ') #ΔΔ')" 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 "Θ; ℬ; Γ ⊢wf (u, τ') #ΔΔ' " using wfD_cons  fresh_DCons setD.simps check_varI check_v_wf  by metis
    ultimately show   "Θ ; Φ ; ℬ ; Γ ; (u, τ') #ΔΔ'  ⊢ s ⇐ τ" using check_varI by auto
  qed
next
  case (check_assignI Θ Φ ℬ Γ Δ u τ v z τ')
  moreover hence "(u, τ) ∈ setD Δ'" by auto
  ultimately show ?case using Typing.check_assignI by simp
next
  case (check_whileI Θ Φ ℬ Γ Δ s1 z s2 τ')
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_seqI Θ Φ ℬ Γ Δ s1 z s2 τ)
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_caseI Θ Φ ℬ Γ Δ 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 Θ  ℬ GNil v b" and  "wfCE Θ  ℬ  ((x, b, TRUE) #Γ GNil) ce2 b'" and "wfCE Θ  ℬ GNil ce1 b'"
  shows ‹Θ; ℬ; (x, b, ([[x ]v]ce  ==  [ v ]ce )) #Γ GNil  ⊨ ce1  ==  ce2 ›
  unfolding valid.simps proof
  have wfg: "Θ ; ℬ  ⊢wf  (x, b, [ [ x ]v ]ce  ==  [ v ]ce ) #Γ GNil" 
    using wfG_cons1I wfG_nilI wfX_wfY assms wf_intros 
    by (meson fresh_GNil wfC_e_eq wfG_intros2)

  show wf: ‹Θ; ℬ; (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 assms wf_replace_inside1(8) assms 
    using wfC_trueI wf_trans(8)  by auto

  show ‹∀i. ((Θ ; (x, b, [ [ x ]v ]ce  ==  [ v ]ce ) #Γ GNil ⊢ i) ∧  (i ⊨ (x, b, [ [ x ]v ]ce  ==  [ v ]ce ) #Γ GNil)  ⟶
             (i ⊨ (ce1  ==  ce2 )))› proof(rule+,goal_cases)
    fix i
    assume as:"Θ ; (x, b, [ [ x ]v ]ce  ==  [ v ]ce ) #Γ GNil ⊢ i ∧  i ⊨ (x, b, [ [ x ]v ]ce  ==  [ v ]ce ) #Γ GNil"
    have 1:"wfV Θ  ℬ ((x, b, [ [ x ]v ]ce  ==  [ v ]ce ) #Γ GNil) v b" 
      using wf_weakening assms append_g.simps toSet.simps wf wfX_wfY 
      by (metis empty_subsetI)
    hence "∃s. i ⟦ v ⟧ ~ s"  using eval_v_exist[OF _ 1] as by auto
    then obtain s where iv:"i⟦ v ⟧ ~ s" ..

    hence ix:"i x = Some s" proof -
      have "i ⊨ [ [ x ]v ]ce  ==  [ v ]ce" using is_satis_g.simps as by auto
      hence "i ⟦ [ [ x ]v ]ce  ==  [ v ]ce ⟧ ~ True" using is_satis.simps by auto
      hence "i ⟦  [ [ x ]v ]ce ⟧ ~ s"  using  
          iv eval_e_elims
        by (metis eval_c_elims(7) eval_e_uniqueness eval_e_valI) 
      thus ?thesis using eval_v_elims(2) eval_e_elims(1) by metis
    qed

    have 1:"wfCE Θ  ℬ ((x, b, [ [ x ]v ]ce  ==  [ v ]ce ) #Γ GNil) ce1 b'" 
      using wfCE_weakening assms append_g.simps toSet.simps wf wfX_wfY 
      by (metis empty_subsetI)
    hence "∃s1. i ⟦ ce1 ⟧ ~ s1"  using eval_e_exist assms as by auto
    then obtain s1 where s1: "i⟦ce1⟧ ~ s1" ..

    moreover have "i⟦ ce2 ⟧ ~ s1" proof -
      have "i⟦ ce2[x::=v]cev ⟧ ~ s1" using assms s1 by auto
      moreover have "ce1 = ce2[x::=v]cev" using subst_v_ce_def assms subst_v_simple_commute by auto
      ultimately have "i(x ↦ s) ⟦ ce2 ⟧ ~ s1" 
        using ix subst_e_eval_v[of i ce1 s1 "ce2[z::=[ x ]v]v" x v s] iv s1 by auto
      moreover have "i(x ↦ s) = i" using ix by auto
      ultimately show ?thesis by auto
    qed
    ultimately show "i ⟦ ce1  ==  ce2 ⟧ ~ True " using eval_c_eqI by metis
  qed
qed


lemma check_v_top:
  fixes v::v
  assumes  "Θ; ℬ; GNil  ⊢ v ⇐ τ" and "ce1 = ce2[z::=v]cev" and  "Θ; ℬ; GNil  ⊢wf  ⦃ z : b_of τ  | ce1 == ce2  ⦄"    
    and "supp ce1 ⊆ supp  ℬ"
  shows "Θ; ℬ; GNil  ⊢ v ⇐ ⦃ z : b_of τ  | ce1 == ce2  ⦄"      
proof -
  obtain t where t: "Θ; ℬ; GNil  ⊢ v ⇒ t ∧ Θ; ℬ; GNil  ⊢ t ≲ τ" 
    using assms check_v_elims by metis

  then obtain z' and b' where *:"t = ⦃ z' : b'  | [ [ z' ]v ]ce  ==  [ v ]ce  ⦄ ∧ atom z' ♯ v ∧ atom z' ♯ (Θ, ℬ,GNil)"
    using assms  infer_v_form by metis
  have beq: "b_of t = b_of τ" using subtype_eq_base2 b_of.simps t by auto 
  obtain x::x where xf: ‹atom x ♯ (Θ, ℬ, GNil, z', [ [ z' ]v ]ce  ==  [ v ]ce , z, ce1  ==  ce2 )› 
    using obtain_fresh by metis

  have "Θ; ℬ; (x, b_of τ, TRUE) #Γ GNil   ⊢wf (ce1[z::=[ x ]v]v  ==  ce2[z::=[ x ]v]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: "Θ; ℬ; (x, b_of t, TRUE) #Γ GNil ⊢wf ce1[z::=[ x ]v]v : b2 ∧ 
            Θ; ℬ; (x, b_of t, TRUE) #Γ GNil ⊢wf ce2[z::=[ x ]v]v : b2" using wfC_elims(3)
    beq by metis

  from xf have "Θ; ℬ; GNil  ⊢ ⦃ z' : b_of t  | [ [ z' ]v ]ce  ==  [ v ]ce  ⦄ ≲  ⦃ z : b_of t  | ce1 == ce2  ⦄" 
  proof  
    show ‹ Θ; ℬ; GNil   ⊢wf ⦃ z' : b_of t  | [ [ z' ]v ]ce  ==  [ v ]ce  ⦄ › using b_of.simps assms infer_v_wf t * by auto
    show ‹ Θ; ℬ; GNil   ⊢wf ⦃ z : b_of t  | ce1  ==  ce2  ⦄ › using beq assms by auto
    have ‹Θ; ℬ; (x, b_of t, ([ [ x ]v ]ce  ==  [ v ]ce )) #Γ GNil  ⊨ (ce1[z::=[ x ]v]v  ==  ce2[z::=[ x ]v]v ) ›  
    proof(rule valid_ce_eq)
      show ‹ce1[z::=[ x ]v]v = ce2[z::=[ x ]v]v[x::=v]cev› proof -
        have "atom z ♯ ce1" using assms fresh_def x_not_in_b_set by fast 
        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 ‹ Θ; ℬ; GNil ⊢wf v : b_of t › using infer_v_wf t by simp
      show  ‹  Θ; ℬ; (x, b_of t, TRUE) #Γ GNil ⊢wf ce2[z::=[ x ]v]v : b2 ›  using b2 by auto

      have " Θ; ℬ; (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 ‹Θ; ℬ; 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  ‹  Θ; ℬ; 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 "Θ; ℬ; (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
qed

end