diff --git a/Normalization.agda b/Normalization.agda
new file mode 100644
index 0000000..434ac33
--- /dev/null
+++ b/Normalization.agda
@@ -0,0 +1,135 @@
+{-# OPTIONS --prop #-}
+
+module Normalization (PV : Set) where
+
+  open import PropUtil
+  open import PropositionalLogic PV
+  open import PropositionalKripke PV
+
+  private
+    variable
+      A  : Form
+      B  : Form
+      F  : Form
+      G  : Form
+      Γ  : Con
+      Γ' : Con
+      x  : PV
+
+  -- ⊢⁰ are neutral forms
+  -- ⊢* are normal forms
+  mutual
+    data _⊢⁰_ : Con → Form → Prop where
+      zero : (A ∷ Γ) ⊢⁰ A
+      next : Γ ⊢⁰ A → (B ∷ Γ) ⊢⁰ A
+      app : Γ ⊢⁰ (A ⇒ B) → Γ ⊢* A → Γ ⊢⁰ B
+    data _⊢*_ : Con → Form → Prop where
+      neu⁰ : Γ ⊢⁰ Var x → Γ ⊢* Var x
+      lam : (A ∷ Γ) ⊢* B → Γ ⊢* (A ⇒ B)
+
+  ⊢⁰→⊢ : Γ ⊢⁰ F → Γ ⊢ F
+  ⊢*→⊢ : Γ ⊢* F → Γ ⊢ F
+  ⊢⁰→⊢ zero = zero
+  ⊢⁰→⊢ (next h) = next (⊢⁰→⊢ h)
+  ⊢⁰→⊢ (app h x) = app (⊢⁰→⊢ h) (⊢*→⊢ x)
+  ⊢*→⊢ (neu⁰ x) = ⊢⁰→⊢ x
+  ⊢*→⊢ (lam h) = lam (⊢*→⊢ h)
+
+  private
+    data _⊆_ : Con → Con → Prop where
+       zero⊆ : Γ ⊆ Γ
+       next⊆ : Γ ⊆ Γ' → Γ ⊆ (A ∷ Γ')
+    retro⊆ : {Γ Γ' : Con} → {A : Form} → (A ∷ Γ) ⊆ Γ' → Γ ⊆ Γ'
+    retro⊆ {Γ' = []} () -- Impossible to have «A∷Γ ⊆ []»
+    retro⊆ {Γ' = x ∷ Γ'} zero⊆ = next⊆ zero⊆
+    retro⊆ {Γ' = x ∷ Γ'} (next⊆ h) = next⊆ (retro⊆ h)
+
+
+  -- Extension of ⊢⁰ to contexts
+  _⊢⁺⁰_ : Con → Con → Prop
+  Γ ⊢⁺⁰ [] = ⊤
+  Γ ⊢⁺⁰ (F ∷ Γ') = (Γ ⊢⁰ F) ∧ (Γ ⊢⁺⁰ Γ')
+  infix 5 _⊢⁺⁰_
+  
+  -- This relation is reflexive
+  private -- Lemma showing that the relation respects ⊆
+    mon⊆≤⁰ : Γ' ⊆ Γ → Γ ⊢⁺⁰ Γ'
+    mon⊆≤⁰ {[]} sub = tt
+    mon⊆≤⁰ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆≤⁰ (next⊆ zero⊆) ⟩
+    mon⊆≤⁰ {x ∷ Γ} (next⊆ sub) = ⟨ (next (proj₁ (mon⊆≤⁰ sub)) ) , mon⊆≤⁰ (next⊆ (retro⊆ sub)) ⟩
+
+  refl⊢⁺⁰ : Γ ⊢⁺⁰ Γ
+  refl⊢⁺⁰ {[]} = tt
+  refl⊢⁺⁰ {x ∷ Γ} = ⟨ zero , mon⊆≤⁰ (next⊆ zero⊆) ⟩
+
+  -- A useful lemma, that we can add hypotheses 
+  addhyp⊢⁺⁰ : Γ ⊢⁺⁰ Γ' → (A ∷ Γ) ⊢⁺⁰ Γ'
+  addhyp⊢⁺⁰ {Γ' = []} h = tt
+  addhyp⊢⁺⁰ {Γ' = A ∷ Γ'} h = ⟨ next (proj₁ h) , addhyp⊢⁺⁰ (proj₂ h) ⟩
+
+
+  {- We use a slightly different Universal Kripke Model -}
+  module UniversalKripke⁰ where
+    Worlds = Con
+    _≤_ : Con → Con → Prop
+    Γ ≤ Η = Η ⊢⁺⁰ Γ
+    _⊩_ : Con → PV → Prop
+    Γ ⊩ x = Γ ⊢⁰ Var x
+
+    refl≤ = refl⊢⁺⁰
+
+    -- Proving transitivity
+    halftran≤* : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺⁰ Γ' → Γ' ⊢* F → Γ ⊢* F
+    halftran≤⁰ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺⁰ Γ' → Γ' ⊢⁰ F → Γ ⊢⁰ F
+    halftran≤* h⁺ (neu⁰ x) = neu⁰ (halftran≤⁰ h⁺ x)
+    halftran≤* h⁺ (lam h) = lam (halftran≤* ⟨ zero , addhyp⊢⁺⁰ h⁺ ⟩ h)
+    halftran≤⁰ h⁺ zero = proj₁ h⁺
+    halftran≤⁰ h⁺ (next h) = halftran≤⁰ (proj₂ h⁺) h
+    halftran≤⁰ h⁺ (app h h') = app (halftran≤⁰ h⁺ h) (halftran≤* h⁺ h')
+    tran≤ : {Γ Γ' Γ'' : Con} → Γ ≤ Γ' → Γ' ≤ Γ'' → Γ ≤ Γ''
+    tran≤ {[]} h h' = tt
+    tran≤ {x ∷ Γ} h h' = ⟨ halftran≤⁰ h' (proj₁ h) , tran≤ (proj₂ h) h' ⟩
+
+    mon⊩ : {w w' : Con} → w ≤ w' → {x : PV} → w ⊩ x → w' ⊩ x
+    mon⊩ h h' = halftran≤⁰ h h'
+
+  
+  ⊢*Var : Γ ⊢* Var x → Γ ⊢⁰ Var x
+  ⊢*Var (neu⁰ x) = x
+
+  UK⁰ : Kripke
+  UK⁰ = record {UniversalKripke⁰}
+  open Kripke UK⁰
+  open UniversalKripke⁰ using (halftran≤⁰)
+
+  -- quote
+  ⊩ᶠ→⊢ : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢* F
+  -- unquote
+  ⊢→⊩ᶠ : {F : Form} → {Γ : Con} → Γ ⊢⁰ F → Γ ⊩ᶠ F
+
+  ⊢→⊩ᶠ {Var x} h = h
+  ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (halftran≤⁰ iq h) (⊩ᶠ→⊢ hF))
+  ⊩ᶠ→⊢ {Var x} h = neu⁰ h
+  ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺⁰ refl⊢⁺⁰) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
+
+  
+--⊩ᶠ→⊢ {F ⇒ G} {Γ} h =  lam (⊩ᶠ→⊢ {G} (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
+  
+  {-
+  ⊩ᶠ→⊢ {F} zero = neu⁰ zero
+  ⊩ᶠ→⊢ {Var x} (next h) = neu⁰ (next {!!})
+  ⊩ᶠ→⊢ {F ⇒ G} (next h) = neu⁰ (next {!!})
+  ⊩ᶠ→⊢ {F ⇒ G} (lam h) = lam (⊩ᶠ→⊢ h)
+  ⊩ᶠ→⊢ {Var x} (app h h₁) = neu⁰ (app {!⊩ᶠ→⊢ h!} (⊩ᶠ→⊢ h₁))
+  ⊩ᶠ→⊢ {F ⇒ G} (app h h₁) = neu⁰ (app {!!} (⊩ᶠ→⊢ h₁))
+  -}
+
+  {-
+  ⊩ᶠ→⊢ {Var x} zero = neu⁰ zero
+  ⊩ᶠ→⊢ {Var x} (next h) = neu⁰ (next (⊢*Var (⊩ᶠ→⊢ {Var x} h)))
+  ⊩ᶠ→⊢ {Var x} (app {A = A} h h₁) = {!!}
+  -- neu⁰ (app {A = A} {!!} (⊩ᶠ→⊢ (CompletenessProof.⊢→⊩ᶠ h₁)))
+  ⊩ᶠ→⊢ {F ⇒ G} {Γ} h = lam (⊩ᶠ→⊢ {G} (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
+  -}
+
+
diff --git a/PropositionalKripke.agda b/PropositionalKripke.agda
index 5720337..4f80c36 100644
--- a/PropositionalKripke.agda
+++ b/PropositionalKripke.agda
@@ -106,15 +106,3 @@ module PropositionalKripke (PV : Set) where
 
     completeness : {F : Form} → [] ⊫ F → [] ⊢ F
     completeness {F} ⊫F = ⊩ᶠ→⊢ (⊫F tt)
-
-    {- Normalization -}
-    norm : [] ⊢ F → [] ⊢ F
-    norm x = completeness (⟦ x ⟧)
-    -- norm is identity ?!
-    idnorm : norm x ≡ x
-    idnorm = ?
-    -- autonorm : (P₁ P₂ : Prop) → (x₁ : P₁) → (norm x₁ : P₂) → P₁ ≡⊢ P₂
-    -- βηnorm : (P₁ P₂ : Prop) → (x₁ : P₁) → (norm x₁ : P₂) → (x₂ : P₂) → norm x₁ ≡ x₂ → P₁ ≡⊢ P₂
-
-    -- autonorm P = {!!}
-    --βηnorm P₁ P₂ = ?
diff --git a/PropositionalLogic.agda b/PropositionalLogic.agda
index 9cefcc0..473e2d1 100644
--- a/PropositionalLogic.agda
+++ b/PropositionalLogic.agda
@@ -47,29 +47,6 @@ module PropositionalLogic (PV : Set) where
 
   infix 5 _⊢_
 
-  -- Equality of derivation
-  infix 2 _≡⊢_
-  data _≡⊢_ : Prop → Prop → Prop where
-    refl : Γ ⊢ A ≡⊢ Γ ⊢ A
-  {-zero≡⊢ : (A ∷ Γ) ⊢ A ≡⊢ (A' ∷ Γ') ⊢ A'
-    next≡⊢ : Γ ⊢ A ≡⊢ Γ' ⊢ A' → (B ∷ Γ) ⊢ A ≡⊢ (B ∷ Γ') ⊢ A'
-    lam≡⊢ : (A ∷ Γ) ⊢ B ≡⊢ (A' ∷ Γ') ⊢ B' →  Γ ⊢ (A ⇒ B) ≡⊢  Γ' ⊢ (A' ⇒ B')
-    app≡⊢ :  Γ ⊢ (A ⇒ B) ≡⊢  Γ' ⊢ (A' ⇒ B') →  Γ ⊢ A ≡⊢ Γ' ⊢ A' → Γ ⊢ B ≡⊢ Γ' ⊢ B'
-  -}
-  {-
-  -- Reflexivity of equality
-  refl≡⊢ : {Γ : Con} → {A : Form} → Γ ⊢ A ≡⊢ Γ ⊢ A
-  refl≡⊢ = {!!}
-
-  -- Symmetry of equality
-  sym≡⊢ : {Γ Γ' : Con} → {A A' : Form} → Γ ⊢ A ≡⊢ Γ' ⊢ A' → Γ' ⊢ A' ≡⊢ Γ ⊢ A
-  sym≡⊢ = {!!}
-
-  -- Transitivity of equality
-  tran≡⊢ : {Γ Γ' Γ'' : Con} → {A A' A'' : Form} → Γ ⊢ A ≡⊢ Γ' ⊢ A' → Γ' ⊢ A' ≡⊢ Γ'' ⊢ A'' → Γ ⊢ A ≡⊢ Γ'' ⊢ A''
-  tran≡⊢ = {!!}
-  -}
-
   -- Extension of ⊢ to contexts
   _⊢⁺_ : Con → Con → Prop
   Γ ⊢⁺ [] = ⊤
diff --git a/prop.agda b/prop.agda
index d67c032..02576e9 100644
--- a/prop.agda
+++ b/prop.agda
@@ -7,91 +7,10 @@ open import Data.String.Properties using (_==_)
 open import Data.List using (List; _∷_; [])
 
 
-{- Prop -}
-
--- ⊥ is a data with no constructor
--- ⊤ is a record with one always-available constructor
-data ⊥ : Prop where
-record ⊤ : Prop where
-  constructor tt
-data _∨_ : Prop → Prop → Prop where
-  inj₁ : {P Q : Prop} → P → P ∨ Q
-  inj₂ : {P Q : Prop} → Q → P ∨ Q
-record _∧_ (P Q : Prop) : Prop where
-  constructor ⟨_,_⟩
-  field
-    p : P
-    q : Q
-infixr 10 _∧_
-infixr 11 _∨_
--- ∧ elimination
-proj₁ : {P Q : Prop} → P ∧ Q → P
-proj₁ pq = _∧_.p pq
-proj₂ : {P Q : Prop} → P ∧ Q → Q
-proj₂ pq = _∧_.q pq
--- ¬ is a shorthand for « → ⊥ »
-¬ : Prop → Prop
-¬ P = P → ⊥
-case⊥ : {P : Prop} → ⊥ → P
-case⊥ ()
--- ∨ elimination
-dis : {P Q S : Prop} → (P ∨ Q) → (P → S) → (Q → S) → S
-dis (inj₁ p) ps qs = ps p
-dis (inj₂ q) ps qs = qs q
-
-
-_⇔_ : Prop → Prop → Prop
-P ⇔ Q = (P → Q) ∧ (Q → P)
-
-
-data Form : Set where
-  Var : String → Form
-  _[⇒]_ : Form → Form → Form
-  
-infixr 8 _[⇒]_
-
-data _≡_ : {A : Set} → A → A → Prop where
-  refl : {A : Set} → {x : A} → x ≡ x
-
-Con = List Form
-
-variable
-  A : Form
-  B : Form
-  C : Form
-  F : Form
-  G : Form
-  Γ : Con
-  Η : Con
-  x : String
-  y : String
-
-data _⊢_ : Con → Form → Prop where
-     zero : (F ∷ Γ) ⊢ F
-     succ : Γ ⊢ F → (G ∷ Γ) ⊢ F
-     lam : (F ∷ Γ) ⊢ G → Γ ⊢ (F [⇒] G)
-     app : Γ ⊢ (F [⇒] G) → Γ ⊢ F → Γ ⊢ G
-
-infixr 5 _⊢_
 
 d-C : [] ⊢ ((Var "Q") [⇒] (Var "R")) [⇒] ((Var "P") [⇒] (Var "Q")) [⇒] (Var "P") [⇒] (Var "R")
 d-C = lam (lam (lam (app (succ (succ zero)) (app (succ zero) zero))))
 
-Env = String → Prop
-
-⟦_⟧F : Form → Env → Prop
-⟦ Var x ⟧F ρ = ρ x
-⟦ A [⇒] B ⟧F ρ = (⟦ A ⟧F ρ) → (⟦ B ⟧F ρ)
-
-⟦_⟧C : Con → Env → Prop
-⟦ [] ⟧C ρ = ⊤
-⟦ A ∷ Γ ⟧C ρ = (⟦ A ⟧F ρ) ∧ (⟦ Γ ⟧C ρ)
-
-⟦_⟧d : Γ ⊢ F → {ρ : Env} → ⟦ Γ ⟧C ρ → ⟦ F ⟧F ρ
-⟦ zero ⟧d p = proj₁ p
-⟦ succ th ⟧d p = ⟦ th ⟧d (proj₂ p)
-⟦ lam th ⟧d = λ pₐ p₀ → ⟦ th ⟧d ⟨ p₀ , pₐ ⟩
-⟦ app th₁ th₂ ⟧d = λ p → ⟦ th₁ ⟧d p (⟦ th₂ ⟧d p)
 
 ρ₀ : Env
 ρ₀ "P" = ⊥
@@ -101,46 +20,6 @@ Env = String → Prop
 cex-d : ([] ⊢ (((Var "P") [⇒] (Var "Q")) [⇒] (Var "P"))) → ⊥
 cex-d h = ⟦ h ⟧d {ρ₀} tt λ x → tt
 
-data ⊢sk : Form → Prop where
-  SS : ⊢sk ((A [⇒] B [⇒] C) [⇒] (A [⇒] B) [⇒] A [⇒] C)
-  KK : ⊢sk (A [⇒] B [⇒] A)
-  app : ⊢sk (A [⇒] B) → ⊢sk A → ⊢sk B
-
-thm : ([] ⊢ A) ⇔ ⊢sk A
-thm₁ :  ⊢sk A → ([] ⊢ A)
-thm₁ SS = lam (lam (lam ( app (app (succ (succ zero)) zero) (app (succ zero) zero))))
-thm₁ KK = lam (lam (succ zero))
-thm₁ (app x x₁) = app (thm₁ x) (thm₁ x₁)
-
-data _⊢skC_ : Con → Form → Prop where
-  zero : (A ∷ Γ) ⊢skC A
-  suc : Γ ⊢skC A → (B ∷ Γ) ⊢skC A
-  SS : Γ ⊢skC ((A [⇒] B [⇒] C) [⇒] (A [⇒] B) [⇒] A [⇒] C)
-  KK : Γ ⊢skC (A [⇒] B [⇒] A)
-  app : Γ ⊢skC (A [⇒] B) → Γ ⊢skC A → Γ ⊢skC B
-
-skC→sk : [] ⊢skC A → ⊢sk A
-skC→sk SS = SS
-skC→sk KK = KK
-skC→sk (app d e) = app (skC→sk d) (skC→sk e)
-
-
-lam-sk : (A ∷ Γ) ⊢skC B → Γ ⊢skC (A [⇒] B)
-lam-sk-zero : Γ ⊢skC (A [⇒] A)
-lam-sk-zero {A = A} = app (app SS KK) (KK {B = A})
-lam-sk zero = lam-sk-zero
-lam-sk (suc x) = app KK x
-lam-sk SS = app KK SS
-lam-sk KK = app KK KK
-lam-sk (app x₁ x₂) = app (app SS (lam-sk x₁)) (lam-sk x₂)
-
-⊢→⊢skC : Γ ⊢ A → Γ ⊢skC A
-⊢→⊢skC zero = zero
-⊢→⊢skC (succ x) = suc (⊢→⊢skC x)
-⊢→⊢skC (lam x) = lam-sk (⊢→⊢skC x)
-⊢→⊢skC (app x x₁) = app (⊢→⊢skC x) (⊢→⊢skC x₁)
-
-thm = ⟨ (λ x → skC→sk (⊢→⊢skC x)) , thm₁ ⟩
 
 
 Pierce = {P Q : Prop} → ((P → Q) → P) → P
@@ -156,35 +35,6 @@ P→TND pierce {P} = pierce {TND P} {⊥} (λ p → case⊥ (nnTND p))
 
 {- Kripke Models -}
 
-record Kripke : Set₁ where
-  field
-    Worlds : Set₀
-    _≤_ : Worlds → Worlds → Prop
-    refl≤ : {w : Worlds} → w ≤ w
-    tran≤ : {a b c : Worlds} → a ≤ b → b ≤ c → a ≤ c
-    _⊩_ : Worlds → String → Prop
-    mon⊩ : {a b : Worlds} → a ≤ b → {p : String} → a ⊩ p → b ⊩ p
-  {- Extending ⊩ to Formulas and Contexts -}
-  _⊩ᶠ_ : Worlds → Form → Prop
-  w ⊩ᶠ Var x = w ⊩ x
-  w ⊩ᶠ (fp [⇒] fq) = {w' : Worlds} → w ≤ w' → w' ⊩ᶠ fp → w' ⊩ᶠ fq
-  mon⊩ᶠ : {a b : Worlds} → a ≤ b → a ⊩ᶠ A → b ⊩ᶠ A
-  mon⊩ᶠ {Var x} ab aA = mon⊩ ab aA
-  mon⊩ᶠ {A [⇒] A₁} ab aA bc cA = aA (tran≤ ab bc) cA
-  _⊩ᶜ_ : Worlds → Con → Prop
-  w ⊩ᶜ [] = ⊤
-  w ⊩ᶜ (p ∷ c) = (w ⊩ᶠ p) ∧ (w ⊩ᶜ c)
-  mon⊩ᶜ : {a b : Worlds} → a ≤ b → a ⊩ᶜ Γ → b ⊩ᶜ Γ
-  mon⊩ᶜ {[]} ab aΓ = aΓ
-  mon⊩ᶜ {A ∷ Γ} ab aΓ = ⟨ mon⊩ᶠ {A} ab (proj₁ aΓ) , mon⊩ᶜ ab (proj₂ aΓ) ⟩
-  _⊫_ : Con → Form → Prop
-  Γ ⊫ F = {w : Worlds} → w ⊩ᶜ Γ → w ⊩ᶠ F
-  {- Soundness -}
-  ⟦_⟧ : Γ ⊢ A → Γ ⊫ A
-  ⟦ zero ⟧ = proj₁
-  ⟦ succ p ⟧ = λ x → ⟦ p ⟧ (proj₂ x)
-  ⟦ lam p ⟧ = λ wΓ w≤ w'A → ⟦ p ⟧ ⟨ w'A , mon⊩ᶜ w≤ wΓ ⟩
-  ⟦ app p p₁ ⟧ wΓ = ⟦ p ⟧ wΓ refl≤ (⟦ p₁ ⟧ wΓ)
 
 {- Pierce is not provable -}
 
@@ -234,65 +84,6 @@ PierceImpliesw₁ h = Kripke.⟦_⟧ PierceW h {PierceWorld.w₁} tt
 NotProvable : ¬([] ⊢ FaultyPierce)
 NotProvable h = Pierce⊥w₁ (PierceImpliesw₁ h)
 
-{- Universal Kripke -}
--- Extension of ⊢ to contexts
-_⊢⁺_ : Con → Con → Prop
-Γ ⊢⁺ [] = ⊤
-Γ ⊢⁺ (F ∷ Γ') = (Γ ⊢ F) ∧ (Γ ⊢⁺ Γ')
-
-module UniversalKripke where
-  Worlds = Con
-  _≤_ : Con → Con → Prop
-  Γ ≤ Η = Η ⊢⁺ Γ
-  _⊩_ : Con → String → Prop
-  Γ ⊩ x = Γ ⊢ Var x
-
-  data _⊆_ : Con → Con → Prop where
-    zero⊆ : Γ ⊆ Γ
-    next⊆ : Γ ⊆ Η → Γ ⊆ (F ∷ Η)
-  retro⊆ : {Γ Γ' : Con} → {F : Form} → (F ∷ Γ) ⊆ Γ' → Γ ⊆ Γ'
-  retro⊆ {Γ' = []} () -- Impossible to have «F∷Γ ⊆ []»
-  retro⊆ {Γ' = x ∷ Γ'} zero⊆ = next⊆ zero⊆
-  retro⊆ {Γ' = x ∷ Γ'} (next⊆ h) = next⊆ (retro⊆ h)
-  mon⊆≤ : {Γ Γ' : Con} → Γ' ⊆ Γ → Γ ⊢⁺ Γ'
-  mon⊆≤ {[]} zero⊆ = tt
-  mon⊆≤ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆≤ (next⊆ zero⊆) ⟩
-  mon⊆≤ {x ∷ Γ} {[]} (next⊆ sub) = tt
-  mon⊆≤ {x ∷ Γ} {y ∷ Γ'} (next⊆ sub) = ⟨ succ (proj₁ (mon⊆≤ sub)) , mon⊆≤ (next⊆ (retro⊆ sub)) ⟩
-
-  refl≤ : {Γ : Con} → Γ ⊢⁺ Γ
-  refl≤ = mon⊆≤ zero⊆
-  addhyp : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺ Γ' → (F ∷ Γ) ⊢⁺ Γ'
-  addhyp {Γ' = []} h = tt
-  addhyp {Γ' = x ∷ Γ'} h = ⟨ succ (proj₁ h) , addhyp (proj₂ h) ⟩
-  halftran≤ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺ Γ' → Γ' ⊢ F → Γ ⊢ F
-  halftran≤ h⁺ zero = proj₁ h⁺
-  halftran≤ h⁺ (succ h) = halftran≤ (proj₂ h⁺) h
-  halftran≤ h⁺ (lam h) = lam (halftran≤ ⟨ zero , addhyp h⁺ ⟩ h)
-  halftran≤ h⁺ (app h h') = app (halftran≤ h⁺ h) (halftran≤ h⁺ h')
-  tran≤ : {Γ Γ' Γ'' : Con} → Γ ≤ Γ' → Γ' ≤ Γ'' → Γ ≤ Γ''
-  tran≤ {[]} h h' = tt
-  tran≤ {x ∷ Γ} h h' = ⟨ halftran≤ h' (proj₁ h) , tran≤ (proj₂ h) h' ⟩
-  
-  mon⊩ : {w w' : Con} → w ≤ w' → {x : String} → w ⊩ x → w' ⊩ x
-  mon⊩ h h' = halftran≤ h h' 
-  
-UK : Kripke
-UK = record {UniversalKripke}
-
-module CompletenessProof where
-  open Kripke UK
-  open UniversalKripke using (mon⊆≤ ; zero⊆ ; next⊆ ; halftran≤ ; addhyp)
-
-  ⊩ᶠ→⊢ : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢ F
-  ⊢→⊩ᶠ : {F : Form} → {Γ : Con} → Γ ⊢ F → Γ ⊩ᶠ F
-  ⊢→⊩ᶠ {Var x} h = h
-  ⊢→⊩ᶠ {F [⇒] F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (lam (app (halftran≤ (addhyp iq) h) zero)) (⊩ᶠ→⊢ hF))
-  ⊩ᶠ→⊢ {Var x} h = h
-  ⊩ᶠ→⊢ {F [⇒] F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (mon⊆≤ (next⊆ zero⊆)) (⊢→⊩ᶠ {F} {F ∷ Γ} zero)))
-
-  completeness : {F : Form} → [] ⊫ F → [] ⊢ F
-  completeness {F} ⊫F = ⊩ᶠ→⊢ (⊫F tt)