(*                                                    *)
(* Formalisation of the chapter on Logical Relations  *)
(* and a Case Study in Equivalence Checking           *)
(* by Karl Crary from the book on Advanced Topics in  *)
(* Types and Programming Languages, MIT Press 2005    *)

(* The formalisation was done by Julien Narboux and   *)
(* Christian Urban.                                   *)

theory Crary
  imports "HOL-Nominal.Nominal"
begin

atom_decl name 

nominal_datatype ty = 
    TBase 
  | TUnit 
  | Arrow "ty" "ty" (‹_→_› [100,100] 100)

nominal_datatype trm = 
    Unit
  | Var "name" (‹Var _› [100] 100)
  | Lam "«name¬trm" (‹Lam [_]._› [100,100] 100)
  | App "trm" "trm" (‹App _ _› [110,110] 100)
  | Const "nat"

type_synonym Ctxt  = "(name×ty) list"
type_synonym Subst = "(name×trm) list" 


lemma perm_ty[simp]: 
  fixes T::"ty"
  and   pi::"name prm"
  shows "pi∙T = T"
  by (induct T rule: ty.induct) (simp_all)

lemma fresh_ty[simp]:
  fixes x::"name" 
  and   T::"ty"
  shows "x♯T"
  by (simp add: fresh_def supp_def)

lemma ty_cases:
  fixes T::ty
  shows "(∃ T₁ T₂. T=T₁→T₂) ∨ T=TUnit ∨ T=TBase"
by (induct T rule:ty.induct) (auto)

instantiation ty :: size
begin

nominal_primrec size_ty
where
  "size (TBase) = 1"
| "size (TUnit) = 1"
| "size (T₁→T₂) = size T₁ + size T₂"
by (rule TrueI)+

instance ..

end

lemma ty_size_greater_zero[simp]:
  fixes T::"ty"
  shows "size T > 0"
by (nominal_induct rule: ty.strong_induct) (simp_all)

section ‹Substitutions›

fun
  lookup :: "Subst → name → trm"   
where
  "lookup [] x = Var x"
| "lookup ((y,T)#θ) x = (if x=y then T else lookup θ x)"

lemma lookup_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi∙(lookup θ x) = lookup (pi∙θ) (pi∙x)"
by (induct θ) (auto simp: perm_bij)

lemma lookup_fresh:
  fixes z::"name"
  assumes a: "z♯θ" "z♯x"
  shows "z♯ lookup θ x"
using a
by (induct rule: lookup.induct) 
   (auto simp: fresh_list_cons)

lemma lookup_fresh':
  assumes a: "z♯θ"
  shows "lookup θ z = Var z"
using a
by (induct rule: lookup.induct)
   (auto simp: fresh_list_cons fresh_prod fresh_atm)
 
nominal_primrec
  psubst :: "Subst → trm → trm"  (‹_🚫› [100,100] 130)
where
  "θ<(Var x)> = (lookup θ x)"
| "θ<(App t₁ t₂)> = App θ<t₁> θ<t₂>"
| "x♯θ ==> θ<(Lam [x].t)> = Lam [x].(θ<t>)"
| "θ<(Const n)> = Const n"
| "θ<(Unit)> = Unit"
  by(finite_guess | simp add: abs_fresh | fresh_guess)+

abbreviation 
 subst :: "trm → name → trm → trm" (‹_[_::=_]› [100,100,100] 100)
where
  "t[x::=t'] ≡ ([(x,t')])<t>" 

lemma subst[simp]:
  shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
  and   "(App t₁ t₂)[y::=t'] = App (t₁[y::=t']) (t₂[y::=t'])"
  and   "x♯(y,t') ==> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
  and   "Const n[y::=t'] = Const n"
  and   "Unit [y::=t'] = Unit"
  by (simp_all add: fresh_list_cons fresh_list_nil)

lemma subst_eqvt[eqvt]:
  fixes pi::"name prm" 
  shows "pi∙(t[x::=t']) = (pi∙t)[(pi∙x)::=(pi∙t')]"
  by (nominal_induct t avoiding: x t' rule: trm.strong_induct)
     (perm_simp add: fresh_bij)+

lemma subst_rename: 
  fixes c::"name"
  assumes a: "c♯t₁"
  shows "t₁[a::=t₂] = ([(c,a)]∙t₁)[c::=t₂]"
using a
  by (nominal_induct t₁ avoiding: a c t₂ rule: trm.strong_induct)
     (auto simp: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)

lemma fresh_psubst: 
  fixes z::"name"
  assumes a: "z♯t" "z♯θ"
  shows "z♯(θ<t>)"
using a
by (nominal_induct t avoiding: z θ t rule: trm.strong_induct)
   (auto simp: abs_fresh lookup_fresh)

lemma fresh_subst'':
  fixes z::"name"
  assumes "z♯t₂"
  shows "z♯t₁[z::=t₂]"
using assms 
by (nominal_induct t₁ avoiding: t₂ z rule: trm.strong_induct)
   (auto simp: abs_fresh fresh_nat fresh_atm)

lemma fresh_subst':
  fixes z::"name"
  assumes "z♯[y].t₁" "z♯t₂"
  shows "z♯t₁[y::=t₂]"
using assms 
by (nominal_induct t₁ avoiding: y t₂ z rule: trm.strong_induct)
   (auto simp: abs_fresh fresh_nat fresh_atm)

lemma fresh_subst:
  fixes z::"name"
  assumes a: "z♯t₁" "z♯t₂"
  shows "z♯t₁[y::=t₂]"
using a 
by (auto simp: fresh_subst' abs_fresh) 

lemma fresh_psubst_simp:
  assumes "x♯t"
  shows "((x,u)#θ)<t> = θ<t>" 
using assms
proof (nominal_induct t avoiding: x u θ rule: trm.strong_induct)
  case (Lam y t x u)
  have fs: "y♯θ" "y♯x" "y♯u" by fact+
  moreover have "x♯ Lam [y].t" by fact 
  ultimately have "x♯t" by (simp add: abs_fresh fresh_atm)
  moreover have ih:"∧n T. n♯t ==> ((n,T)#θ)<t> = θ<t>" by fact
  ultimately have "((x,u)#θ)<t> = θ<t>" by auto
  moreover have "((x,u)#θ)<Lam [y].t> = Lam [y].(((x,u)#θ)<t>)" using fs 
    by (simp add: fresh_list_cons fresh_prod)
  moreover have " θ<Lam [y].t> = Lam [y]. (θ<t>)" using fs by simp
  ultimately show "((x,u)#θ)<Lam [y].t> = θ<Lam [y].t>" by auto
qed (auto simp: fresh_atm abs_fresh)

lemma forget: 
  fixes x::"name"
  assumes a: "x♯t" 
  shows "t[x::=t'] = t"
  using a
by (nominal_induct t avoiding: x t' rule: trm.strong_induct)
   (auto simp: fresh_atm abs_fresh)

lemma subst_fun_eq:
  fixes u::trm
  assumes h:"[x].t₁ = [y].t₂"
  shows "t₁[x::=u] = t₂[y::=u]"
proof -
  { 
    assume "x=y" and "t₁=t₂"
    then have ?thesis using h by simp
  }
  moreover 
  {
    assume h1:"x ≠ y" and h2:"t₁=[(x,y)] ∙ t₂" and h3:"x ♯ t₂"
    then have "([(x,y)] ∙ t₂)[x::=u] = t₂[y::=u]" by (simp add: subst_rename)
    then have ?thesis using h2 by simp 
  }
  ultimately show ?thesis using alpha h by blast
qed

lemma psubst_empty[simp]:
  shows "[]<t> = t"
by (nominal_induct t rule: trm.strong_induct) 
   (auto simp: fresh_list_nil)

lemma psubst_subst_psubst:
  assumes h:"c♯θ"
  shows "θ<t>[c::=s] = ((c,s)#θ)<t>"
  using h
by (nominal_induct t avoiding: θ c s rule: trm.strong_induct)
   (auto simp: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)

lemma subst_fresh_simp:
  assumes a: "x♯θ"
  shows "θ<Var x> = Var x"
using a
by (induct θ arbitrary: x) (auto simp:fresh_list_cons fresh_prod fresh_atm)

lemma psubst_subst_propagate: 
  assumes "x♯θ" 
  shows "θ<t[x::=u]> = θ<t>[x::=θ<u>]"
using assms
proof (nominal_induct t avoiding: x u θ rule: trm.strong_induct)
  case (Var n x u θ)
  { assume "x=n"
    moreover have "x♯θ" by fact 
    ultimately have "θ<Var n[x::=u]> = θ<Var n>[x::=θ<u>]" using subst_fresh_simp by auto
  }
  moreover 
  { assume h:"x≠n"
    then have "x♯Var n" by (auto simp: fresh_atm) 
    moreover have "x♯θ" by fact
    ultimately have "x♯θ<Var n>" using fresh_psubst by blast
    then have " θ<Var n>[x::=θ<u>] = θ<Var n>" using forget by auto
    then have "θ<Var n[x::=u]> = θ<Var n>[x::=θ<u>]" using h by auto
  }
  ultimately show ?case by auto  
next
  case (Lam n t x u θ)
  have fs:"n♯x" "n♯u" "n♯θ" "x♯θ" by fact+
  have ih:"∧ y s θ. y♯θ ==> ((θ<(t[y::=s])>) = ((θ<t>)[y::=(θ<s>)]))" by fact
  have "θ <(Lam [n].t)[x::=u]> = θ<Lam [n]. (t [x::=u])>" using fs by auto
  then have "θ <(Lam [n].t)[x::=u]> = Lam [n]. θ<t [x::=u]>" using fs by auto
  moreover have "θ<t[x::=u]> = θ<t>[x::=θ<u>]" using ih fs by blast
  ultimately have "θ <(Lam [n].t)[x::=u]> = Lam [n].(θ<t>[x::=θ<u>])" by auto
  moreover have "Lam [n].(θ<t>[x::=θ<u>]) = (Lam [n].θ<t>)[x::=θ<u>]" using fs fresh_psubst by auto
  ultimately have "θ<(Lam [n].t)[x::=u]> = (Lam [n].θ<t>)[x::=θ<u>]" using fs by auto
  then show "θ<(Lam [n].t)[x::=u]> = θ<Lam [n].t>[x::=θ<u>]" using fs by auto
qed (auto)

section ‹Typing›

inductive
  valid :: "Ctxt → bool"
where
  v_nil[intro]:  "valid []"
| v_cons[intro]: "[valid Γ;a♯Γ] ==> valid ((a,T)#Γ)"

equivariance valid 

inductive_cases
  valid_cons_elim_auto[elim]:"valid ((x,T)#Γ)"

abbreviation
  "sub_context" :: "Ctxt → Ctxt → bool" (‹ _ ⊆ _ › [55,55] 55)
where
  "Γ₁ ⊆ Γ₂ ≡ ∀a T. (a,T)∈set Γ₁ ⟶ (a,T)∈set Γ₂"

lemma valid_monotonicity[elim]:
 fixes Γ Γ' :: Ctxt
 assumes a: "Γ ⊆ Γ'" 
 and     b: "x♯Γ'"
 shows "(x,T₁)#Γ ⊆ (x,T₁)#Γ'"
using a b by auto

lemma fresh_context: 
  fixes  Γ :: "Ctxt"
  and    a :: "name"
  assumes "a♯Γ"
  shows "¬(∃τ::ty. (a,τ)∈set Γ)"
using assms 
by (induct Γ)
   (auto simp: fresh_prod fresh_list_cons fresh_atm)

lemma type_unicity_in_context:
  assumes a: "valid Γ" 
  and     b: "(x,T₁) ∈ set Γ" 
  and     c: "(x,T₂) ∈ set Γ"
  shows "T₁=T₂"
using a b c
by (induct Γ)
   (auto dest!: fresh_context)

inductive
  typing :: "Ctxt→trm→ty→bool" (‹ _ ⊨ _ : _ › [60,60,60] 60) 
where
  T_Var[intro]:   "[valid Γ; (x,T)∈set Γ] ==> Γ ⊨ Var x : T"
| T_App[intro]:   "[Γ ⊨ e₁ : T₁→T₂; Γ ⊨ e₂ : T₁] ==> Γ ⊨ App e₁ e₂ : T₂"
| T_Lam[intro]:   "[x♯Γ; (x,T₁)#Γ ⊨ t : T₂] ==> Γ ⊨ Lam [x].t : T₁→T₂"
| T_Const[intro]: "valid Γ ==> Γ ⊨ Const n : TBase"
| T_Unit[intro]:  "valid Γ ==> Γ ⊨ Unit : TUnit"

equivariance typing

nominal_inductive typing
  by (simp_all add: abs_fresh)

lemma typing_implies_valid:
  assumes a: "Γ ⊨ t : T"
  shows "valid Γ"
  using a by (induct) (auto)

declare trm.inject [simp add]
declare ty.inject  [simp add]

inductive_cases typing_inv_auto[elim]:
  "Γ ⊨ Lam [x].t : T"
  "Γ ⊨ Var x : T"
  "Γ ⊨ App x y : T"
  "Γ ⊨ Const n : T"
  "Γ ⊨ Unit : TUnit"
  "Γ ⊨ s : TUnit"

declare trm.inject [simp del]
declare ty.inject [simp del]


section ‹Definitional Equivalence›

inductive
  def_equiv :: "Ctxt→trm→trm→ty→bool" (‹_ ⊨ _ ≡ _ : _› [60,60] 60) 
where
  Q_Refl[intro]:  "Γ ⊨ t : T ==> Γ ⊨ t ≡ t : T"
| Q_Symm[intro]:  "Γ ⊨ t ≡ s : T ==> Γ ⊨ s ≡ t : T"
| Q_Trans[intro]: "[Γ ⊨ s ≡ t : T; Γ ⊨ t ≡ u : T] ==> Γ ⊨ s ≡ u : T"
| Q_Abs[intro]:   "[x♯Γ; (x,T₁)#Γ ⊨ s₂ ≡ t₂ : T₂] ==> Γ ⊨ Lam [x]. s₂ ≡ Lam [x]. t₂ : T₁ → T₂"
| Q_App[intro]:   "[Γ ⊨ s₁ ≡ t₁ : T₁ → T₂ ; Γ ⊨ s₂ ≡ t₂ : T₁] ==> Γ ⊨ App s₁ s₂ ≡ App t₁ t₂ : T₂"
| Q_Beta[intro]:  "[x♯(Γ,s₂,t₂); (x,T₁)#Γ ⊨ s₁ ≡ t₁ : T₂ ; Γ ⊨ s₂ ≡ t₂ : T₁]
                   ==> Γ ⊨ App (Lam [x]. s₁) s₂ ≡ t₁[x::=t₂] : T₂"
| Q_Ext[intro]:   "[x♯(Γ,s,t); (x,T₁)#Γ ⊨ App s (Var x) ≡ App t (Var x) : T₂]
                   ==> Γ ⊨ s ≡ t : T₁ → T₂"
| Q_Unit[intro]:  "[Γ ⊨ s : TUnit; Γ ⊨ t: TUnit] ==> Γ ⊨ s ≡ t : TUnit"

equivariance def_equiv

nominal_inductive def_equiv
  by (simp_all add: abs_fresh fresh_subst'')

lemma def_equiv_implies_valid:
  assumes a: "Γ ⊨ t ≡ s : T"
  shows "valid Γ"
using a by (induct) (auto elim: typing_implies_valid)

section ‹Weak Head Reduction›

inductive
  whr_def :: "trm→trm→bool" (‹_ ↝ _› [80,80] 80) 
where
  QAR_Beta[intro]: "App (Lam [x]. t₁) t₂ ↝ t₁[x::=t₂]"
| QAR_App[intro]:  "t₁ ↝ t₁' ==> App t₁ t₂ ↝ App t₁' t₂"

declare trm.inject  [simp add]
declare ty.inject  [simp add]

inductive_cases whr_inv_auto[elim]: 
  "t ↝ t'"
  "Lam [x].t ↝ t'"
  "App (Lam [x].t12) t2 ↝ t"
  "Var x ↝ t"
  "Const n ↝ t"
  "App p q ↝ t"
  "t ↝ Const n"
  "t ↝ Var x"
  "t ↝ App p q"

declare trm.inject  [simp del]
declare ty.inject  [simp del]

equivariance whr_def

section ‹Weak Head Normalisation›

abbreviation 
 nf :: "trm → bool" (‹_ ↝|› [100] 100)
where
  "t↝| ≡ ¬(∃ u. t ↝ u)" 

inductive
  whn_def :: "trm→trm→bool" (‹_ ⇓ _› [80,80] 80) 
where
  QAN_Reduce[intro]: "[s ↝ t; t ⇓ u] ==> s ⇓ u"
| QAN_Normal[intro]: "t↝| ==> t ⇓ t"

declare trm.inject[simp]

inductive_cases whn_inv_auto[elim]: "t ⇓ t'"

declare trm.inject[simp del]

equivariance whn_def

lemma red_unicity : 
  assumes a: "x ↝ a" 
  and     b: "x ↝ b"
  shows "a=b"
  using a b
by (induct arbitrary: b) (use subst_fun_eq in blast)+

lemma nf_unicity :
  assumes "x ⇓ a" and "x ⇓ b"
  shows "a=b"
  using assms 
proof (induct arbitrary: b)
  case (QAN_Reduce x t a b)
  have h:"x ↝ t" "t ⇓ a" by fact+
  have ih:"∧b. t ⇓ b ==> a = b" by fact
  obtain t' where "x ↝ t'" and hl:"t' ⇓ b" using h ‹x ⇓ b› by auto
  then have "t=t'" using h red_unicity by auto
  then show "a=b" using ih hl by auto
qed (auto)


section ‹Algorithmic Term Equivalence and Algorithmic Path Equivalence›

inductive
  alg_equiv :: "Ctxt→trm→trm→ty→bool" (‹_ ⊨ _ ⇔ _ : _› [60,60,60,60] 60) 
and
  alg_path_equiv :: "Ctxt→trm→trm→ty→bool" (‹_ ⊨ _ ↔ _ : _› [60,60,60,60] 60) 
where
  QAT_Base[intro]:  "[s ⇓ p; t ⇓ q; Γ ⊨ p ↔ q : TBase] ==> Γ ⊨ s ⇔ t : TBase"
| QAT_Arrow[intro]: "[x♯(Γ,s,t); (x,T₁)#Γ ⊨ App s (Var x) ⇔ App t (Var x) : T₂]
                     ==> Γ ⊨ s ⇔ t : T₁ → T₂"
| QAT_One[intro]:   "valid Γ ==> Γ ⊨ s ⇔ t : TUnit"
| QAP_Var[intro]:   "[valid Γ;(x,T) ∈ set Γ] ==> Γ ⊨ Var x ↔ Var x : T"
| QAP_App[intro]:   "[Γ ⊨ p ↔ q : T₁ → T₂; Γ ⊨ s ⇔ t : T₁] ==> Γ ⊨ App p s ↔ App q t : T₂"
| QAP_Const[intro]: "valid Γ ==> Γ ⊨ Const n ↔ Const n : TBase"

equivariance alg_equiv

nominal_inductive alg_equiv
  avoids QAT_Arrow: x
  by simp_all

declare trm.inject [simp add]
declare ty.inject  [simp add]

inductive_cases alg_equiv_inv_auto[elim]: 
  "Γ ⊨ s⇔t : TBase"
  "Γ ⊨ s⇔t : T₁ → T₂"
  "Γ ⊨ s↔t : TBase"
  "Γ ⊨ s↔t : TUnit"
  "Γ ⊨ s↔t : T₁ → T₂"

  "Γ ⊨ Var x ↔ t : T"
  "Γ ⊨ Var x ↔ t : T'"
  "Γ ⊨ s ↔ Var x : T"
  "Γ ⊨ s ↔ Var x : T'"
  "Γ ⊨ Const n ↔ t : T"
  "Γ ⊨ s ↔ Const n : T"
  "Γ ⊨ App p s ↔ t : T"
  "Γ ⊨ s ↔ App q t : T"
  "Γ ⊨ Lam[x].s ↔ t : T"
  "Γ ⊨ t ↔ Lam[x].s : T"

declare trm.inject [simp del]
declare ty.inject [simp del]

lemma Q_Arrow_strong_inversion:
  assumes fs: "x♯Γ" "x♯t" "x♯u" 
  and h: "Γ ⊨ t ⇔ u : T₁→T₂"
  shows "(x,T₁)#Γ ⊨ App t (Var x) ⇔ App u (Var x) : T₂"
proof -
  obtain y where fs2: "y♯(Γ,t,u)" and "(y,T₁)#Γ ⊨ App t (Var y) ⇔ App u (Var y) : T₂" 
    using h by auto
  then have "([(x,y)]∙((y,T₁)#Γ)) ⊨ [(x,y)]∙ App t (Var y) ⇔ [(x,y)]∙ App u (Var y) : T₂" 
    using  alg_equiv.eqvt[simplified] by blast
  then show ?thesis using fs fs2 by (perm_simp)
qed

(*
Warning this lemma is false:

lemma algorithmic_type_unicity:
  shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
  and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"

Here is the counter example : 
\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase and \<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : TUnit
*)

lemma algorithmic_path_type_unicity:
  shows "Γ ⊨ s ↔ t : T ==> Γ ⊨ s ↔ u : T' ==> T = T'"
proof (induct arbitrary:  u T' 
       rule: alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _  "%a b c d . True"    ])
  case (QAP_Var Γ x T u T')
  have "Γ ⊨ Var x ↔ u : T'" by fact
  then have "u=Var x" and "(x,T') ∈ set Γ" by auto
  moreover have "valid Γ" "(x,T) ∈ set Γ" by fact+
  ultimately show "T=T'" using type_unicity_in_context by auto
next
  case (QAP_App Γ p q T₁ T₂ s t u T₂')
  have ih:"∧u T. Γ ⊨ p ↔ u : T ==> T₁→T₂ = T" by fact
  have "Γ ⊨ App p s ↔ u : T₂'" by fact
  then obtain r t T₁' where "u = App r t"  "Γ ⊨ p ↔ r : T₁' → T₂'" by auto
  with ih have "T₁→T₂ = T₁' → T₂'" by auto
  then show "T₂=T₂'" using ty.inject by auto
qed (auto)

lemma alg_path_equiv_implies_valid:
  shows  "Γ ⊨ s ⇔ t : T ==> valid Γ" 
  and    "Γ ⊨ s ↔ t : T ==> valid Γ"
by (induct rule : alg_equiv_alg_path_equiv.inducts) auto

lemma algorithmic_symmetry:
  shows "Γ ⊨ s ⇔ t : T ==> Γ ⊨ t ⇔ s : T" 
  and   "Γ ⊨ s ↔ t : T ==> Γ ⊨ t ↔ s : T"
by (induct rule: alg_equiv_alg_path_equiv.inducts) 
   (auto simp: fresh_prod)

lemma algorithmic_transitivity:
  shows "Γ ⊨ s ⇔ t : T ==> Γ ⊨ t ⇔ u : T ==> Γ ⊨ s ⇔ u : T"
  and   "Γ ⊨ s ↔ t : T ==> Γ ⊨ t ↔ u : T ==> Γ ⊨ s ↔ u : T"
proof (nominal_induct Γ s t T and Γ s t T avoiding: u rule: alg_equiv_alg_path_equiv.strong_inducts)
  case (QAT_Base s p t q Γ u)
  have "Γ ⊨ t ⇔ u : TBase" by fact
  then obtain r' q' where b1: "t ⇓ q'" and b2: "u ⇓ r'" and b3: "Γ ⊨ q' ↔ r' : TBase" by auto
  have ih: "Γ ⊨ q ↔ r' : TBase ==> Γ ⊨ p ↔ r' : TBase" by fact
  have "t ⇓ q" by fact
  with b1 have eq: "q=q'" by (simp add: nf_unicity)
  with ih b3 have "Γ ⊨ p ↔ r' : TBase" by simp
  moreover
  have "s ⇓ p" by fact
  ultimately show "Γ ⊨ s ⇔ u : TBase" using b2 by auto
next
  case (QAT_Arrow  x Γ s t T₁ T₂ u)
  have ih:"(x,T₁)#Γ ⊨ App t (Var x) ⇔ App u (Var x) : T₂
                                   ==> (x,T₁)#Γ ⊨ App s (Var x) ⇔ App u (Var x) : T₂" by fact
  have fs: "x♯Γ" "x♯s" "x♯t" "x♯u" by fact+
  have "Γ ⊨ t ⇔ u : T₁→T₂" by fact
  then have "(x,T₁)#Γ ⊨ App t (Var x) ⇔ App u (Var x) : T₂" using fs 
    by (simp add: Q_Arrow_strong_inversion)
  with ih have "(x,T₁)#Γ ⊨ App s (Var x) ⇔ App u (Var x) : T₂" by simp
  then show "Γ ⊨ s ⇔ u : T₁→T₂" using fs by (auto simp: fresh_prod)
next
  case (QAP_App Γ p q T₁ T₂ s t u)
  have "Γ ⊨ App q t ↔ u : T₂" by fact
  then obtain r T₁' v where ha: "Γ ⊨ q ↔ r : T₁'→T₂" and hb: "Γ ⊨ t ⇔ v : T₁'" and eq: "u = App r v" 
    by auto
  have ih1: "Γ ⊨ q ↔ r : T₁→T₂ ==> Γ ⊨ p ↔ r : T₁→T₂" by fact
  have ih2:"Γ ⊨ t ⇔ v : T₁ ==> Γ ⊨ s ⇔ v : T₁" by fact
  have "Γ ⊨ p ↔ q : T₁→T₂" by fact
  then have "Γ ⊨ q ↔ p : T₁→T₂" by (simp add: algorithmic_symmetry)
  with ha have "T₁'→T₂ = T₁→T₂" using algorithmic_path_type_unicity by simp
  then have "T₁' = T₁" by (simp add: ty.inject) 
  then have "Γ ⊨ s ⇔ v : T₁" "Γ ⊨ p ↔ r : T₁→T₂" using ih1 ih2 ha hb by auto
  then show "Γ ⊨ App p s ↔ u : T₂" using eq by auto
qed (auto)

lemma algorithmic_weak_head_closure:
  shows "Γ ⊨ s ⇔ t : T ==> s' ↝ s ==> t' ↝ t ==> Γ ⊨ s' ⇔ t' : T"
proof (nominal_induct Γ s t T avoiding: s' t'  
    rule: alg_equiv_alg_path_equiv.strong_inducts(1) [of _ _ _ _ "λa b c d e. True"])
qed(auto intro!: QAT_Arrow)

lemma algorithmic_monotonicity:
  shows "Γ ⊨ s ⇔ t : T ==> Γ ⊆ Γ' ==> valid Γ' ==> Γ' ⊨ s ⇔ t : T"
  and   "Γ ⊨ s ↔ t : T ==> Γ ⊆ Γ' ==> valid Γ' ==> Γ' ⊨ s ↔ t : T"
proof (nominal_induct Γ s t T and Γ s t T avoiding: Γ' rule: alg_equiv_alg_path_equiv.strong_inducts)
 case (QAT_Arrow x Γ s t T₁ T₂ Γ')
  have fs:"x♯Γ" "x♯s" "x♯t" "x♯Γ'" by fact+
  have h2:"Γ ⊆ Γ'" by fact
  have ih:"∧Γ'. [(x,T₁)#Γ ⊆ Γ'; valid Γ'] ==> Γ' ⊨ App s (Var x) ⇔ App t (Var x) : T₂" by fact
  have "valid Γ'" by fact
  then have "valid ((x,T₁)#Γ')" using fs by auto
  moreover
  have sub: "(x,T₁)#Γ ⊆ (x,T₁)#Γ'" using h2 by auto
  ultimately have "(x,T₁)#Γ' ⊨ App s (Var x) ⇔ App t (Var x) : T₂" using ih by simp
  then show "Γ' ⊨ s ⇔ t : T₁→T₂" using fs by (auto simp: fresh_prod)
qed (auto)

lemma path_equiv_implies_nf:
  assumes "Γ ⊨ s ↔ t : T"
  shows "s ↝|" and "t ↝|"
using assms
by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto)

section ‹Logical Equivalence›

function log_equiv :: "(Ctxt → trm → trm → ty → bool)" (‹_ ⊨ _ is _ : _› [60,60,60,60] 60) 
where    
   "Γ ⊨ s is t : TUnit = True"
 | "Γ ⊨ s is t : TBase = Γ ⊨ s ⇔ t : TBase"
 | "Γ ⊨ s is t : (T₁ → T₂) =
    (∀Γ' s' t'. Γ⊆Γ' ⟶ valid Γ' ⟶ Γ' ⊨ s' is t' : T₁ ⟶ (Γ' ⊨ (App s s') is (App t t') : T₂))"
using ty_cases by (force simp: ty.inject)+

termination by lexicographic_order

lemma logical_monotonicity:
 fixes Γ Γ' :: Ctxt
 assumes a1: "Γ ⊨ s is t : T" 
 and     a2: "Γ ⊆ Γ'" 
 and     a3: "valid Γ'"
 shows "Γ' ⊨ s is t : T"
using a1 a2 a3
proof (induct arbitrary: Γ' rule: log_equiv.induct)
  case (2 Γ s t Γ')
  then show "Γ' ⊨ s is t : TBase" using algorithmic_monotonicity by auto
next
  case (3 Γ s t T₁ T₂ Γ')
  have "Γ ⊨ s is t : T₁→T₂" 
  and  "Γ ⊆ Γ'" 
  and  "valid Γ'" by fact+
  then show "Γ' ⊨ s is t : T₁→T₂" by simp
qed (auto)

lemma main_lemma:
  shows "Γ ⊨ s is t : T ==> valid Γ ==> Γ ⊨ s ⇔ t : T" 
    and "Γ ⊨ p ↔ q : T ==> Γ ⊨ p is q : T"
proof (nominal_induct T arbitrary: Γ s t p q rule: ty.strong_induct)
  case (Arrow T₁ T₂)
  { 
    case (1 Γ s t)
    have ih1:"∧Γ s t. [Γ ⊨ s is t : T₂; valid Γ] ==> Γ ⊨ s ⇔ t : T₂" by fact
    have ih2:"∧Γ s t. Γ ⊨ s ↔ t : T₁ ==> Γ ⊨ s is t : T₁" by fact
    have h:"Γ ⊨ s is t : T₁→T₂" by fact
    obtain x::name where fs:"x♯(Γ,s,t)" by (erule exists_fresh[OF fs_name1])
    have "valid Γ" by fact
    then have v: "valid ((x,T₁)#Γ)" using fs by auto
    then have "(x,T₁)#Γ ⊨ Var x ↔ Var x : T₁" by auto
    then have "(x,T₁)#Γ ⊨ Var x is Var x : T₁" using ih2 by auto
    then have "(x,T₁)#Γ ⊨ App s (Var x) is App t (Var x) : T₂" using h v by auto
    then have "(x,T₁)#Γ ⊨ App s (Var x) ⇔ App t (Var x) : T₂" using ih1 v by auto
    then show "Γ ⊨ s ⇔ t : T₁→T₂" using fs by (auto simp: fresh_prod)
  next
    case (2 Γ p q)
    have h: "Γ ⊨ p ↔ q : T₁→T₂" by fact
    have ih1:"∧Γ s t. Γ ⊨ s ↔ t : T₂ ==> Γ ⊨ s is t : T₂" by fact
    have ih2:"∧Γ s t. [Γ ⊨ s is t : T₁; valid Γ] ==> Γ ⊨ s ⇔ t : T₁" by fact
    {
      fix Γ' s t
      assume "Γ ⊆ Γ'" and hl:"Γ' ⊨ s is t : T₁" and hk: "valid Γ'"
      then have "Γ' ⊨ p ↔ q : T₁ → T₂" using h algorithmic_monotonicity by auto
      moreover have "Γ' ⊨ s ⇔ t : T₁" using ih2 hl hk by auto
      ultimately have "Γ' ⊨ App p s ↔ App q t : T₂" by auto
      then have "Γ' ⊨ App p s is App q t : T₂" using ih1 by auto
    }
    then show "Γ ⊨ p is q : T₁→T₂"  by simp
  }
next
  case TBase
  { case 2
    have h:"Γ ⊨ s ↔ t : TBase" by fact
    then have "s ↝|" and "t ↝|" using path_equiv_implies_nf by auto
    then have "s ⇓ s" and "t ⇓ t" by auto
    then have "Γ ⊨ s ⇔ t : TBase" using h by auto
    then show "Γ ⊨ s is t : TBase" by auto
  }
qed (auto elim: alg_path_equiv_implies_valid) 

corollary corollary_main:
  assumes a: "Γ ⊨ s ↔ t : T"
  shows "Γ ⊨ s ⇔ t : T"
using a main_lemma alg_path_equiv_implies_valid by blast

lemma logical_symmetry:
  assumes a: "Γ ⊨ s is t : T"
  shows "Γ ⊨ t is s : T"
using a 
by (nominal_induct arbitrary: Γ s t rule: ty.strong_induct) 
   (auto simp: algorithmic_symmetry)

lemma logical_transitivity:
  assumes "Γ ⊨ s is t : T" "Γ ⊨ t is u : T" 
  shows "Γ ⊨ s is u : T"
using assms
proof (nominal_induct arbitrary: Γ s t u  rule:ty.strong_induct)
  case TBase
  then show "Γ ⊨ s is u : TBase" by (auto elim:  algorithmic_transitivity)
next 
  case (Arrow T₁ T₂ Γ s t u)
  have h1:"Γ ⊨ s is t : T₁ → T₂" by fact
  have h2:"Γ ⊨ t is u : T₁ → T₂" by fact
  have ih1:"∧Γ s t u. [Γ ⊨ s is t : T₁; Γ ⊨ t is u : T₁] ==> Γ ⊨ s is u : T₁" by fact
  have ih2:"∧Γ s t u. [Γ ⊨ s is t : T₂; Γ ⊨ t is u : T₂] ==> Γ ⊨ s is u : T₂" by fact
  {
    fix Γ' s' u'
    assume hsub:"Γ ⊆ Γ'" and hl:"Γ' ⊨ s' is u' : T₁" and hk: "valid Γ'"
    then have "Γ' ⊨ u' is s' : T₁" using logical_symmetry by blast
    then have "Γ' ⊨ u' is u' : T₁" using ih1 hl by blast
    then have "Γ' ⊨ App t u' is App u u' : T₂" using h2 hsub hk by auto
    moreover have "Γ' ⊨ App s s' is App t u' : T₂" using h1 hsub hl hk by auto
    ultimately have "Γ' ⊨ App s s' is App u u' : T₂" using ih2 by blast
  }
  then show "Γ ⊨ s is u : T₁ → T₂" by auto
qed (auto)

lemma logical_weak_head_closure:
  assumes a: "Γ ⊨ s is t : T" 
  and     b: "s' ↝ s" 
  and     c: "t' ↝ t"
  shows "Γ ⊨ s' is t' : T"
using a b c algorithmic_weak_head_closure 
proof (nominal_induct arbitrary: Γ s t s' t' rule: ty.strong_induct)
next
  case (Arrow ty1 ty2)
  then show ?case
    by (smt (verit, ccfv_threshold) QAR_App log_equiv.simps(3))
qed auto
   

lemma logical_weak_head_closure':
  assumes "Γ ⊨ s is t : T" and "s' ↝ s" 
  shows "Γ ⊨ s' is t : T"
using assms
proof (nominal_induct arbitrary: Γ s t s' rule: ty.strong_induct)
  case (TBase  Γ s t s')
  then show ?case by force
next
  case (TUnit Γ s t s')
  then show ?case by auto
next 
  case (Arrow T₁ T₂ Γ s t s')
  have h1:"s' ↝ s" by fact
  have ih:"∧Γ s t s'. [Γ ⊨ s is t : T₂; s' ↝ s] ==> Γ ⊨ s' is t : T₂" by fact
  have h2:"Γ ⊨ s is t : T₁→T₂" by fact
  then 
  have hb:"∀Γ' s' t'. Γ⊆Γ' ⟶ valid Γ' ⟶ Γ' ⊨ s' is t' : T₁ ⟶ (Γ' ⊨ (App s s') is (App t t') : T₂)" 
    by auto
  {
    fix Γ' s₂ t₂
    assume "Γ ⊆ Γ'" and "Γ' ⊨ s₂ is t₂ : T₁" and "valid Γ'"
    then have "Γ' ⊨ (App s s₂) is (App t t₂) : T₂" using hb by auto
    moreover have "(App s' s₂) ↝ (App s s₂)" using h1 by auto  
    ultimately have "Γ' ⊨ App s' s₂ is App t t₂ : T₂" using ih by auto
  }
  then show "Γ ⊨ s' is t : T₁→T₂" by auto
qed 

abbreviation 
 log_equiv_for_psubsts :: "Ctxt → Subst → Subst → Ctxt → bool"  (‹_ ⊨ _ is _ over _› [60,60] 60) 
where
  "Γ' ⊨ θ is θ' over Γ ≡ ∀x T. (x,T) ∈ set Γ ⟶ Γ' ⊨ θ<Var x> is θ'<Var x> : T"

lemma logical_pseudo_reflexivity:
  assumes "Γ' ⊨ t is s over Γ"
  shows "Γ' ⊨ s is s over Γ"
  by (meson assms logical_symmetry logical_transitivity) 

lemma logical_subst_monotonicity :
  fixes Γ Γ' Γ'' :: Ctxt
  assumes a: "Γ' ⊨ θ is θ' over Γ" 
  and     b: "Γ' ⊆ Γ''"
  and     c: "valid Γ''"
  shows "Γ'' ⊨ θ is θ' over Γ"
using a b c logical_monotonicity by blast

lemma equiv_subst_ext :
  assumes h1: "Γ' ⊨ θ is θ' over Γ" 
  and     h2: "Γ' ⊨ s is t : T" 
  and     fs: "x♯Γ"
  shows "Γ' ⊨ (x,s)#θ is (x,t)#θ' over (x,T)#Γ"
using assms
proof -
  {
    fix y U
    assume "(y,U) ∈ set ((x,T)#Γ)"
    moreover
    { 
      assume "(y,U) ∈ set [(x,T)]"
      with h2 have "Γ' ⊨ ((x,s)#θ)<Var y> is ((x,t)#θ')<Var y> : U" by auto 
    }
    moreover
    {
      assume hl:"(y,U) ∈ set Γ"
      then have "¬ y♯Γ" by (induct Γ) (auto simp: fresh_list_cons fresh_atm fresh_prod)
      then have hf:"x♯ Var y" using fs by (auto simp: fresh_atm)
      then have "((x,s)#θ)<Var y> = θ<Var y>" "((x,t)#θ')<Var y> = θ'<Var y>" 
        using fresh_psubst_simp by blast+ 
      moreover have  "Γ' ⊨ θ<Var y> is θ'<Var y> : U" using h1 hl by auto
      ultimately have "Γ' ⊨ ((x,s)#θ)<Var y> is ((x,t)#θ')<Var y> : U" by auto
    }
    ultimately have "Γ' ⊨ ((x,s)#θ)<Var y> is ((x,t)#θ')<Var y> : U" by auto
  }
  then show "Γ' ⊨ (x,s)#θ is (x,t)#θ' over (x,T)#Γ" by auto
qed

theorem fundamental_theorem_1:
  assumes a1: "Γ ⊨ t : T" 
  and     a2: "Γ' ⊨ θ is θ' over Γ"
  and     a3: "valid Γ'" 
  shows "Γ' ⊨ θ<t> is θ'<t> : T"   
using a1 a2 a3
proof (nominal_induct Γ t T avoiding: θ θ' arbitrary: Γ' rule: typing.strong_induct)
  case (T_Lam x Γ T₁ t₂ T₂ θ θ' Γ')
  have vc: "x♯θ" "x♯θ'" "x♯Γ" by fact+
  have asm1: "Γ' ⊨ θ is θ' over Γ" by fact
  have ih:"∧θ θ' Γ'. [Γ' ⊨ θ is θ' over (x,T₁)#Γ; valid Γ'] ==> Γ' ⊨ θ<t₂> is θ'<t₂> : T₂" by fact
  show "Γ' ⊨ θ<Lam [x].t₂> is θ'<Lam [x].t₂> : T₁→T₂" using vc
  proof (simp, intro strip)
    fix Γ'' s' t'
    assume sub: "Γ' ⊆ Γ''" 
    and    asm2: "Γ''⊨ s' is t' : T₁" 
    and    val: "valid Γ''"
    from asm1 val sub have "Γ'' ⊨ θ is θ' over Γ" using logical_subst_monotonicity by blast
    with asm2 vc have "Γ'' ⊨ (x,s')#θ is (x,t')#θ' over (x,T₁)#Γ" using equiv_subst_ext by blast
    with ih val have "Γ'' ⊨ ((x,s')#θ)<t₂> is ((x,t')#θ')<t₂> : T₂" by auto
    with vc have "Γ''⊨θ<t₂>[x::=s'] is θ'<t₂>[x::=t'] : T₂" by (simp add: psubst_subst_psubst)
    moreover 
    have "App (Lam [x].θ<t₂>) s' ↝ θ<t₂>[x::=s']" by auto
    moreover 
    have "App (Lam [x].θ'<t₂>) t' ↝ θ'<t₂>[x::=t']" by auto
    ultimately show "Γ''⊨ App (Lam [x].θ<t₂>) s' is App (Lam [x].θ'<t₂>) t' : T₂" 
      using logical_weak_head_closure by auto
  qed
qed (auto)


theorem fundamental_theorem_2:
  assumes h1: "Γ ⊨ s ≡ t : T" 
  and     h2: "Γ' ⊨ θ is θ' over Γ"
  and     h3: "valid Γ'"
  shows "Γ' ⊨ θ<s> is θ'<t> : T"
using h1 h2 h3
proof (nominal_induct Γ s t T avoiding: Γ' θ θ' rule: def_equiv.strong_induct)
  case (Q_Refl Γ t T Γ' θ θ')
  then show "Γ' ⊨ θ<t> is θ'<t> : T" using fundamental_theorem_1
    by blast
next
  case (Q_Symm Γ t s T Γ' θ θ')
  then show "Γ' ⊨ θ<s> is θ'<t> : T" using logical_symmetry by blast
next
  case (Q_Trans Γ s t T u Γ' θ θ')
  have ih1: "∧ Γ' θ θ'. [Γ' ⊨ θ is θ' over Γ; valid Γ'] ==> Γ' ⊨ θ<s> is θ'<t> : T" by fact
  have ih2: "∧ Γ' θ θ'. [Γ' ⊨ θ is θ' over Γ; valid Γ'] ==> Γ' ⊨ θ<t> is θ'<u> : T" by fact
  have h: "Γ' ⊨ θ is θ' over Γ" 
  and  v: "valid Γ'" by fact+
  then have "Γ' ⊨ θ' is θ' over Γ" using logical_pseudo_reflexivity by auto
  then have "Γ' ⊨ θ'<t> is θ'<u> : T" using ih2 v by auto
  moreover have "Γ' ⊨ θ<s> is θ'<t> : T" using ih1 h v by auto
  ultimately show "Γ' ⊨ θ<s> is θ'<u> : T" using logical_transitivity by blast
next
  case (Q_Abs x Γ T₁ s₂ t₂ T₂ Γ' θ θ')
  have fs:"x♯Γ" by fact
  have fs2: "x♯θ" "x♯θ'" by fact+
  have h2: "Γ' ⊨ θ is θ' over Γ" 
  and  h3: "valid Γ'" by fact+
  have ih:"∧Γ' θ θ'. [Γ' ⊨ θ is θ' over (x,T₁)#Γ; valid Γ'] ==> Γ' ⊨ θ<s₂> is θ'<t₂> : T₂" by fact
  {
    fix Γ'' s' t'
    assume "Γ' ⊆ Γ''" and hl:"Γ''⊨ s' is t' : T₁" and hk: "valid Γ''"
    then have "Γ'' ⊨ θ is θ' over Γ" using h2 logical_subst_monotonicity by blast
    then have "Γ'' ⊨ (x,s')#θ is (x,t')#θ' over (x,T₁)#Γ" using equiv_subst_ext hl fs by blast
    then have "Γ'' ⊨ ((x,s')#θ)<s₂> is ((x,t')#θ')<t₂> : T₂" using ih hk by blast
    then have "Γ''⊨ θ<s₂>[x::=s'] is θ'<t₂>[x::=t'] : T₂" using fs2 psubst_subst_psubst by auto
    moreover have "App (Lam [x]. θ<s₂>) s' ↝ θ<s₂>[x::=s']" 
              and "App (Lam [x].θ'<t₂>) t' ↝ θ'<t₂>[x::=t']" by auto
    ultimately have "Γ'' ⊨ App (Lam [x]. θ<s₂>) s' is App (Lam [x].θ'<t₂>) t' : T₂" 
      using logical_weak_head_closure by auto
  }
  moreover have "valid Γ'" by fact
  ultimately have "Γ' ⊨ Lam [x].θ<s₂> is Lam [x].θ'<t₂> : T₁→T₂" by auto
  then show "Γ' ⊨ θ<Lam [x].s₂> is θ'<Lam [x].t₂> : T₁→T₂" using fs2 by auto
next
  case (Q_App Γ s₁ t₁ T₁ T₂ s₂ t₂ Γ' θ θ')
  then show "Γ' ⊨ θ<App s₁ s₂> is θ'<App t₁ t₂> : T₂" by auto 
next
  case (Q_Beta x Γ s₂ t₂ T₁ s12 t12 T₂ Γ' θ θ')
  have h: "Γ' ⊨ θ is θ' over Γ" 
  and  h': "valid Γ'" by fact+
  have fs: "x♯Γ" by fact
  have fs2: " x♯θ" "x♯θ'" by fact+
  have ih1: "∧Γ' θ θ'. [Γ' ⊨ θ is θ' over Γ; valid Γ'] ==> Γ' ⊨ θ<s₂> is θ'<t₂> : T₁" by fact
  have ih2: "∧Γ' θ θ'. [Γ' ⊨ θ is θ' over (x,T₁)#Γ; valid Γ'] ==> Γ' ⊨ θ<s12> is θ'<t12> : T₂" by fact
  have "Γ' ⊨ θ<s₂> is θ'<t₂> : T₁" using ih1 h' h by auto
  then have "Γ' ⊨ (x,θ<s₂>)#θ is (x,θ'<t₂>)#θ' over (x,T₁)#Γ" using equiv_subst_ext h fs by blast
  then have "Γ' ⊨ ((x,θ<s₂>)#θ)<s12> is ((x,θ'<t₂>)#θ')<t12> : T₂" using ih2 h' by auto
  then have "Γ' ⊨ θ<s12>[x::=θ<s₂>] is θ'<t12>[x::=θ'<t₂>] : T₂" using fs2 psubst_subst_psubst by auto
  then have "Γ' ⊨ θ<s12>[x::=θ<s₂>] is θ'<t12[x::=t₂]> : T₂" using fs2 psubst_subst_propagate by auto
  moreover have "App (Lam [x].θ<s12>) (θ<s₂>) ↝ θ<s12>[x::=θ<s₂>]" by auto 
  ultimately have "Γ' ⊨ App (Lam [x].θ<s12>) (θ<s₂>) is θ'<t12[x::=t₂]> : T₂" 
    using logical_weak_head_closure' by auto
  then show "Γ' ⊨ θ<App (Lam [x].s12) s₂> is θ'<t12[x::=t₂]> : T₂" using fs2 by simp
next
  case (Q_Ext x Γ s t T₁ T₂ Γ' θ θ')
  have h2: "Γ' ⊨ θ is θ' over Γ" 
  and  h2': "valid Γ'" by fact+
  have fs:"x♯Γ" "x♯s" "x♯t" by fact+
  have ih:"∧Γ' θ θ'. [Γ' ⊨ θ is θ' over (x,T₁)#Γ; valid Γ']
                          ==> Γ' ⊨ θ<App s (Var x)> is θ'<App t (Var x)> : T₂" by fact
   {
    fix Γ'' s' t'
    assume hsub: "Γ' ⊆ Γ''" and hl: "Γ''⊨ s' is t' : T₁" and hk: "valid Γ''"
    then have "Γ'' ⊨ θ is θ' over Γ" using h2 logical_subst_monotonicity by blast
    then have "Γ'' ⊨ (x,s')#θ is (x,t')#θ' over (x,T₁)#Γ" using equiv_subst_ext hl fs by blast
    then have "Γ'' ⊨ ((x,s')#θ)<App s (Var x)> is ((x,t')#θ')<App t (Var x)> : T₂" using ih hk by blast
    then 
    have "Γ'' ⊨ App (((x,s')#θ)<s>) (((x,s')#θ)<(Var x)>) is App (((x,t')#θ')<t>) (((x,t')#θ')<(Var x)>) : T₂"
      by auto
    then have "Γ'' ⊨ App ((x,s')#θ)<s> s' is App ((x,t')#θ')<t> t' : T₂" by auto
    then have "Γ'' ⊨ App (θ<s>) s' is App (θ'<t>) t' : T₂" using fs fresh_psubst_simp by auto
  }
  moreover have "valid Γ'" by fact
  ultimately show "Γ' ⊨ θ<s> is θ'<t> : T₁→T₂" by auto
next
  case (Q_Unit Γ s t Γ' θ θ')  
  then show "Γ' ⊨ θ<s> is θ'<t> : TUnit" by auto
qed


theorem completeness:
  assumes asm: "Γ ⊨ s ≡ t : T"
  shows   "Γ ⊨ s ⇔ t : T"
proof -
  have val: "valid Γ" using def_equiv_implies_valid asm by simp
  then have "Γ ⊨ [] is [] over Γ"
    by (simp add: QAP_Var main_lemma(2)) 
  then have "Γ ⊨ []<s> is []<t> : T" using fundamental_theorem_2 val asm by blast
  then have "Γ ⊨ s is t : T" by simp
  then show  "Γ ⊨ s ⇔ t : T" using main_lemma(1) val by simp
qed

text ‹We leave soundness as an exercise - just like Crary in the ATS book :-) \\
 @{prop[mode=IfThen] "[Γ ⊨ s ⇔ t : T; Γ ⊨ t : T; Γ ⊨ s : T] ==> Γ ⊨ s ≡ t : T"} \\
 prop‹[Γ ⊨ s ↔ t : T; Γ ⊨ t : T; Γ ⊨ s : T] ==> Γ ⊨ s ≡ t : T›
 ›

end