Reverted to previous status and re-write logic with dumb forall -> Infinitary Logic

FirstOrderLogic.agda

@@ -1,108 +0,0 @@
-{-# OPTIONS --prop #-}
-
-open import Agda.Builtin.Nat
-open import Agda.Builtin.Bool
-open import Agda.Primitive using (Level)
-
-module FirstOrderLogic (TV : Set) (TV= : TV → TV → Bool) (F : Nat → Set) (R : Nat → Set) where
-
-  open import PropUtil
-  open import ListUtil
-
-  mutual
-    data Args : Nat → Set where
-      zero : Args 0
-      next : {n : Nat} → Args n → Term → Args (suc n)
-    data Term : Set where
-      Var : TV → Term
-      Fun : {n : Nat} → F n → Args n → Term
-      
-  private
-    variable
-      n : Nat
-
-  if : {ℓ : Level} → {T : Set ℓ} → Bool → T → T → T
-  if true a b = a
-  if false a b = b
-  
-  mutual
-    [_/_]ᵗ : Term → TV → Term → Term
-    [_/_]ᵃ : Term → TV → Args n → Args n
-    [ t / x ]ᵗ (Var x') = if (TV= x x') t (Var x')
-    [ t / x ]ᵗ (Fun f A) = Fun f ([ t / x ]ᵃ A)
-    [ t / x ]ᵃ zero = zero
-    [ t / x ]ᵃ (next A t₁) = next ([ t / x ]ᵃ A) ([ t / x ]ᵗ t₁)
-
-  -- A ⊂sub B if B can be obtained with finite substitution from A
-  data _⊂sub_ : Args n → Args n → Prop where
-    zero : {A : Args n} → A ⊂sub A
-    next : {A B : Args n} → {t : Term} → {x : TV} → A ⊂sub B → A ⊂sub ([ t / x ]ᵃ B)
-
-  tran⊂sub : {A B C : Args n} → A ⊂sub B → B ⊂sub C → A ⊂sub C
-  tran⊂sub zero h₂ = h₂
-  tran⊂sub h₁ zero = h₁
-  tran⊂sub h₁ (next h₂) = next (tran⊂sub h₁ h₂)
-
-  data Form : Set where
-    Rel : {n : Nat} → R n → (Args n) → Form
-    _⇒_ : Form → Form → Form
-    _∧∧_ : Form → Form → Form
-    ⊤⊤   : Form
-    ∀∀ : TV → Form → Form
-    
-  infixr 10 _∧∧_
-  infixr 8 _⇒_
-  
-  Con = List Form
-
-  private
-    variable
-      A   : Form
-      A'  : Form
-      B   : Form
-      B'  : Form
-      C   : Form
-      Γ   : Con
-      Γ'  : Con
-      Γ'' : Con
-      Δ   : Con
-      Δ'  : Con
-      x   : TV
-      t   : Term
-
-  [_/_] : Term → TV → Form → Form
-  [ t / x ] (Rel r tz) = Rel r ([ t / x ]ᵃ tz)
-  [ t / x ] (A ⇒ A₁) = ([ t / x ] A) ⇒ ([ t / x ] A₁)
-  [ t / x ] (A ∧∧ A₁) = ([ t / x ] A) ∧∧ ([ t / x ] A₁)
-  [ t / x ] ⊤⊤ = ⊤⊤
-  [ t / x ] (∀∀ x₁ A) = if (TV= x x₁) A ([ t / x ] A)
-
-  mutual
-    _∉FVᵗ_ : TV → Term → Prop
-    _∉FVᵃ_ : TV → Args n → Prop
-    x ∉FVᵗ Var x₁ = if (TV= x x₁) ⊥ ⊤
-    x ∉FVᵗ Fun f A = x ∉FVᵃ A
-    x ∉FVᵃ zero = ⊤
-    x ∉FVᵃ next A t = (x ∉FVᵃ A) ∧ (x ∉FVᵗ t)
-  _∉FVᶠ_ : TV → Form → Prop
-  x ∉FVᶠ Rel R A = x ∉FVᵃ A
-  x ∉FVᶠ (A ⇒ A₁) = x ∉FVᶠ A ∧ x ∉FVᶠ A₁
-  x ∉FVᶠ (A ∧∧ A₁) = x ∉FVᶠ A ∧ x ∉FVᶠ A₁
-  x ∉FVᶠ ⊤⊤ = ⊤
-  x ∉FVᶠ ∀∀ x₁ A = if (TV= x x₁) ⊤ (x ∉FVᶠ A)
-  _∉FVᶜ_ : TV → Con → Prop
-  x ∉FVᶜ [] = ⊤
-  x ∉FVᶜ (A ∷ Γ) = x ∉FVᶠ A ∧ x ∉FVᶜ Γ
-  
-  data _⊢_ : Con → Form → Prop where
-    zero : A ∈ Γ → Γ ⊢ A
-    lam : (A ∷ Γ) ⊢ B → Γ ⊢ (A ⇒ B)
-    app : Γ ⊢ (A ⇒ B) → Γ ⊢ A → Γ ⊢ B
-    andi : Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧∧ B
-    ande₁ : Γ ⊢ A ∧∧ B → Γ ⊢ A
-    ande₂ : Γ ⊢ A ∧∧ B → Γ ⊢ B
-    true : Γ ⊢ ⊤⊤
-    ∀-i : x ∉FVᶜ Γ → Γ ⊢ A → Γ ⊢ ∀∀ x A
-    ∀-e : Γ ⊢ ∀∀ x A → Γ ⊢ [ t / x ] A 
-
-  infix 5 _⊢_

InfinitaryFirstOrderKripke.agda

@@ -1,20 +1,17 @@
-{-# OPTIONS --prop --no-termination-check #-}
+{-# OPTIONS --prop #-}
 
 open import Agda.Builtin.Nat
-open import Agda.Builtin.Bool
 
-module FirstOrderKripke (PV : Set) (TV : Set) (TV= : TV → TV → Bool) (Fu : Nat → Set) (R : Nat → Set) where
+module PropositionalKripke (Term : Set) (R : Nat → Set) where
 
   open import ListUtil
   open import PropUtil
-  open import FirstOrderLogic TV TV= Fu R
+  open import FirstOrderLogic Term R
 
   private
     variable
-      n : Nat
+      x : Term
-      t : Term
+      y : Term
-      x : TV
-      y : TV
       F : Form
       G : Form
       Γ : Con
@@ -28,8 +25,8 @@ module FirstOrderKripke (PV : Set) (TV : Set) (TV= : TV → TV → Bool) (Fu : N
       _≤_ : Worlds → Worlds → Prop
       refl≤ : {w : Worlds} → w ≤ w
       tran≤ : {a b c : Worlds} → a ≤ b → b ≤ c → a ≤ c
-      _⊩_[_] : Worlds → R n → Args n → Prop
+      _⊩_[_] : Worlds → {n : Nat} → R n → Args n → Prop
-      mon⊩ : {a b : Worlds} → a ≤ b → {r : R n} {A : Args n} → a ⊩ r [ A ] → b ⊩ r [ A ]
+      mon⊩ : {a b : Worlds} → a ≤ b → {n : Nat} → {r : R n} → {A : Args n} → a ⊩ r [ A ] → b ⊩ r [ A ]
 
     private
       variable
@@ -40,13 +37,12 @@ module FirstOrderKripke (PV : Set) (TV : Set) (TV= : TV → TV → Bool) (Fu : N
         w₃ : Worlds
     
     {- Extending ⊩ to Formulas and Contexts -}
-    -- It is in fact
     _⊩ᶠ_ : Worlds → Form → Prop
-    w ⊩ᶠ (Rel {n = n} r A) = {B : Args n} → A ⊂sub B → w ⊩ r [ B ]
+    w ⊩ᶠ (Rel r A) = w ⊩ r [ A ]
     w ⊩ᶠ (fp ⇒ fq) = {w' : Worlds} → w ≤ w' → w' ⊩ᶠ fp → w' ⊩ᶠ fq
     w ⊩ᶠ (fp ∧∧ fq) = w ⊩ᶠ fp ∧ w ⊩ᶠ fq
     w ⊩ᶠ ⊤⊤ = ⊤
-    w ⊩ᶠ (∀∀ x F) = (t : Term) → w ⊩ᶠ ([ t / x ] F)
+    w ⊩ᶠ ∀∀ F = { t : Term } → w ⊩ᶠ F t
     
     _⊩ᶜ_ : Worlds → Con → Prop
     w ⊩ᶜ [] = ⊤
@@ -54,11 +50,11 @@ module FirstOrderKripke (PV : Set) (TV : Set) (TV= : TV → TV → Bool) (Fu : N
     
     -- The extensions are monotonous
     mon⊩ᶠ : w ≤ w' → w ⊩ᶠ F → w' ⊩ᶠ F
-    mon⊩ᶠ {F = Rel r A} ww' wF s = mon⊩ ww' (wF s)
+    mon⊩ᶠ {F = Rel r A} ww' wF = mon⊩ ww' wF
     mon⊩ᶠ {F = F ⇒ G} ww' wF w'w'' w''F = wF (tran≤ ww' w'w'') w''F
     mon⊩ᶠ {F = F ∧∧ G} ww' ⟨ wF , wG ⟩ = ⟨ mon⊩ᶠ {F = F} ww' wF , mon⊩ᶠ {F = G} ww' wG ⟩
     mon⊩ᶠ {F = ⊤⊤} ww' wF = tt
-    mon⊩ᶠ {F = ∀∀ x F} ww' wF t = mon⊩ᶠ {F = [ t / x ] F} ww' (wF t)
+    mon⊩ᶠ {F = ∀∀ F} ww' wF {t} = mon⊩ᶠ {F = F t} ww' (wF {t})
   
     mon⊩ᶜ : w ≤ w' → w ⊩ᶜ Γ → w' ⊩ᶜ Γ
     mon⊩ᶜ {Γ = []} ww' wΓ = wΓ
@@ -69,15 +65,6 @@ module FirstOrderKripke (PV : Set) (TV : Set) (TV= : TV → TV → Bool) (Fu : N
     Γ ⊫ F = {w : Worlds} → w ⊩ᶜ Γ → w ⊩ᶠ F
 
     {- Soundness -}
-    th' : w ⊩ᶠ F → w ⊩ᶠ [ t / x ] F
-    th' {F = Rel r A} h {B} s = h {B} (tran⊂sub (next zero) s)
-    th' {F = F ⇒ F₁} h o hF = {!h o ?!}
-    th' {F = F ∧∧ F₁} h = {!!}
-    th' {F = ⊤⊤} h = {!!}
-    th' {F = ∀∀ x F} h = {!!}
-    th : Γ ⊫ F → Γ ⊫ [ t / x ] F
-    th {[]} h _ = {!!}
-    th {x ∷ Γ} h = {!!}
     ⟦_⟧ : Γ ⊢ F → Γ ⊫ F
     ⟦ zero zero∈ ⟧ wΓ = proj₁ wΓ
     ⟦ zero (next∈ h) ⟧ wΓ = ⟦ zero h ⟧ (proj₂ wΓ)
@@ -87,5 +74,5 @@ module FirstOrderKripke (PV : Set) (TV : Set) (TV= : TV → TV → Bool) (Fu : N
     ⟦ ande₁ p ⟧ wΓ = proj₁ $ ⟦ p ⟧ wΓ
     ⟦ ande₂ p ⟧ wΓ = proj₂ $ ⟦ p ⟧ wΓ
     ⟦ true ⟧ wΓ = tt
-    ⟦ ∀-i i p ⟧ wΓ t = {!⟦ p ⟧!}
+    ⟦ ∀i p ⟧ wΓ {t} = ⟦ p {t} ⟧ wΓ
-    ⟦ ∀-e {t = t} p ⟧ wΓ = ⟦ p ⟧ wΓ t
+    ⟦ ∀e p {t} ⟧ wΓ = ⟦ p ⟧ wΓ {t}

InfinitaryFirstOrderKripkeGeneral.agda

@@ -0,0 +1,180 @@
+{-# OPTIONS --prop #-}
+
+open import Agda.Builtin.Nat hiding (zero)
+
+module PropositionalKripkeGeneral (Term : Set) (R : Nat → Set) where
+
+  open import ListUtil
+  open import PropUtil
+  open import FirstOrderLogic Term R using (Form; Args; Rel; _⇒_; _∧∧_; ⊤⊤; ∀∀; Con)
+
+  open import PropositionalKripke Term R using (Kripke)
+
+  record Preorder (T : Set₀) : Set₁ where
+    constructor order
+    field
+      _≤_ : T → T → Prop
+      refl≤ : {a : T} → a ≤ a
+      tran≤ : {a b c : T} → a ≤ b → b ≤ c → a ≤ c
+
+  [_]ᵒᵖ : {T : Set₀} → Preorder T → Preorder T
+  [_]ᵒᵖ o = order (λ a b → (Preorder._≤_ o) b a) (Preorder.refl≤ o) (λ h₁ h₂ → (Preorder.tran≤ o) h₂ h₁)
+
+  record NormalAndNeutral : Set₁ where
+    field
+      _⊢⁰_ : Con → Form → Prop
+      _⊢*_ : Con → Form → Prop
+      zero : {Γ : Con} → {F : Form} → (F ∷ Γ) ⊢⁰ F
+      app : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ⇒ G) → Γ ⊢* F → Γ ⊢⁰ G
+      ande₁ : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ∧∧ G) → Γ ⊢⁰ F
+      ande₂ : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ∧∧ G) → Γ ⊢⁰ G
+      ∀e : {Γ : Con} → {F : Term → Form} → Γ ⊢⁰ (∀∀ F) → ( {t : Term} → Γ ⊢⁰ (F t) )
+      neu⁰ : {Γ : Con} → {n : Nat} → {r : R n} → {A : Args n} → Γ ⊢⁰ Rel r A → Γ ⊢* Rel r A
+      lam : {Γ : Con} → {F G : Form} → (F ∷ Γ) ⊢* G → Γ ⊢* (F ⇒ G)
+      andi : {Γ : Con} → {F G : Form} → Γ ⊢* F → Γ ⊢* G → Γ ⊢* (F ∧∧ G)
+      ∀i : {Γ : Con} → {F : Term → Form} → ({t : Term} → Γ ⊢* F t) → Γ ⊢* ∀∀ F
+      true : {Γ : Con} → Γ ⊢* ⊤⊤
+
+  record NormalizationFrame : Set₁ where
+    field
+      o : Preorder Con
+      nn : NormalAndNeutral
+      retro : {Γ Δ : Con} → {F : Form} → (Preorder._≤_ o) Γ Δ → (Preorder._≤_ o) Γ (F ∷ Δ)
+      ⊢tran : {Γ Δ : Con} → {F : Form} → (Preorder._≤_ o) Γ Δ → (NormalAndNeutral._⊢⁰_ nn) Γ F → (NormalAndNeutral._⊢⁰_ nn) Δ F
+
+    open Preorder o
+    open NormalAndNeutral nn
+
+  
+    UK : Kripke
+    UK = record {
+       Worlds = Con;
+       _≤_ = _≤_;
+       refl≤ = refl≤;
+       tran≤ = tran≤;
+       _⊩_[_] = λ Γ r A → Γ ⊢⁰ Rel r A;
+       mon⊩ = λ Γ h → ⊢tran Γ h
+       }
+
+    open Kripke UK
+    
+    -- q is quote, u is unquote
+    q : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢* F
+    u : {F : Form} → {Γ : Con} → Γ ⊢⁰ F → Γ ⊩ᶠ F
+  
+    u {Rel r A} h = h
+    u {F ⇒ F₁} h {Γ'} iq hF = u {F₁} (app {Γ'} {F} {F₁} (⊢tran iq h) (q hF))
+    u {F ∧∧ G} h = ⟨ (u {F} (ande₁ h)) , (u {G} (ande₂ h)) ⟩
+    u {⊤⊤} h = tt
+    u {∀∀ F} h {t} = u {F t} (∀e h {t})
+    
+    q {Rel r A} h = neu⁰ h
+    q {F ⇒ F₁} {Γ} h = lam (q (h (retro (Preorder.refl≤ o)) (u {F} {F ∷ Γ} zero)))
+    q {F ∧∧ G} ⟨ hF , hG ⟩ = andi (q {F} hF) (q {G} hG)
+    q {⊤⊤} h = true
+    q {∀∀ F} h = ∀i λ {t} → q {F t} h
+
+
+  module NormalizationTests where
+
+    {- Now using our records -}
+    open import FirstOrderLogic Term R hiding (Form; _⇒_; Con)
+
+
+    ClassicNN : NormalAndNeutral
+    ClassicNN = record
+      {
+      _⊢⁰_ = _⊢⁰_ ;
+      _⊢*_ = _⊢*_ ;
+      zero = zero zero∈ ;
+      app = app ;
+      ande₁ = ande₁;
+      ande₂ = ande₂ ;
+      neu⁰ = neu⁰ ;
+      lam = lam ;
+      andi = andi ;
+      true = true ;
+      ∀i = ∀i ;
+      ∀e = ∀e
+      }
+
+    BiggestNN : NormalAndNeutral
+    BiggestNN = record
+      {
+      _⊢⁰_ = _⊢_ ;
+      _⊢*_ = _⊢_ ;
+      zero = zero zero∈ ;
+      app = app ;
+      ande₁ = ande₁ ;
+      ande₂ = ande₂ ;
+      neu⁰ = λ x → x ;
+      lam = lam ;
+      andi = andi ;
+      true = true ;
+      ∀i = ∀i ;
+      ∀e = ∀e
+      }
+
+    PO⊢⁺  = [ order {Con} _⊢⁺_  refl⊢⁺  tran⊢⁺  ]ᵒᵖ
+    PO⊢⁰⁺ = [ order {Con} _⊢⁰⁺_ refl⊢⁰⁺ tran⊢⁰⁺ ]ᵒᵖ
+    PO∈*  = order {Con} _∈*_  refl∈*  tran∈*
+    PO⊂⁺  = order {Con} _⊂⁺_  refl⊂⁺  tran⊂⁺
+    PO⊂   = order {Con} _⊂_   refl⊂   tran⊂
+    PO⊆   = order {Con} _⊆_   refl⊆   tran⊆
+    
+    -- Completeness Proofs
+    Frame⊢ : NormalizationFrame
+    Frame⊢ = record
+      {
+      o = PO⊢⁺ ;
+      nn = BiggestNN ;
+      retro = λ s → addhyp⊢⁺ (right∈* refl∈*) s ;
+      ⊢tran = halftran⊢⁺
+      }
+
+    Frame⊢⁰ : NormalizationFrame
+    Frame⊢⁰ = record
+      {
+      o = PO⊢⁰⁺ ;
+      nn = ClassicNN ;
+      retro = λ s → addhyp⊢⁰⁺ (right∈* refl∈*) s ;
+      ⊢tran = halftran⊢⁰⁺⁰
+      }
+
+    Frame∈* : NormalizationFrame
+    Frame∈* = record
+      {
+      o = PO∈* ;
+      nn = ClassicNN ;
+      retro = right∈* ;
+      ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ s) h
+      }
+
+    Frame⊂⁺ : NormalizationFrame
+    Frame⊂⁺ = record
+      {
+      o = PO⊂⁺ ;
+      nn = ClassicNN ;
+      retro = next⊂⁺ ;
+      ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* s) h
+      }
+
+    Frame⊂ : NormalizationFrame
+    Frame⊂ = record
+      {
+      o = PO⊂ ;
+      nn = ClassicNN ;
+      retro = next⊂ ;
+      ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* $ ⊂→⊂⁺ s) h
+      }
+
+    Frame⊆ : NormalizationFrame
+    Frame⊆ = record
+      {
+      o = PO⊆ ;
+      nn = ClassicNN ;
+      retro = next⊆ ;
+      ⊢tran =  λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* $ ⊂→⊂⁺ $ ⊆→⊂ s) h
+      }
+
+    

InfinitaryFirstOrderLogic.agda

@@ -0,0 +1,190 @@
+{-# OPTIONS --prop #-}
+
+open import Agda.Builtin.Nat
+
+module FirstOrderLogic (Term : Set) (R : Nat → Set) where
+
+  open import PropUtil
+  open import ListUtil
+
+  data Args : Nat → Set where
+    zero : Args 0
+    next : {n : Nat} → Args n → Term → Args (suc n)
+    
+  data Form : Set where
+    Rel : {n : Nat} → R n → (Args n) → Form
+    _⇒_ : Form → Form → Form
+    _∧∧_ : Form → Form → Form
+    ∀∀ : (Term → Form) → Form
+    ⊤⊤ : Form
+    
+  infixr 10 _∧∧_
+  infixr 8 _⇒_
+
+
+  Con = List Form
+
+  -- Proofs
+
+  private
+    variable
+      A B : Form
+      Γ Γ' Γ'' Δ : Con
+      n : Nat
+      r : R n
+      ts : Args n
+
+  data _⊢_ : Con → Form → Prop where
+    zero : A ∈ Γ → Γ ⊢ A
+    lam : (A ∷ Γ) ⊢ B → Γ ⊢ (A ⇒ B)
+    app : Γ ⊢ (A ⇒ B) → Γ ⊢ A → Γ ⊢ B
+    andi : Γ ⊢ A → Γ ⊢ B → Γ ⊢ (A ∧∧ B)
+    ande₁ : Γ ⊢ (A ∧∧ B) → Γ ⊢ A
+    ande₂ : Γ ⊢ (A ∧∧ B) → Γ ⊢ B
+    true : Γ ⊢ ⊤⊤
+    ∀i : {F : Term → Form} → ({t : Term} → Γ ⊢ F t) → Γ ⊢ (∀∀ F)
+    ∀e : {F : Term → Form} → Γ ⊢ (∀∀ F) → ( {t : Term} → Γ ⊢ (F t) )
+
+
+
+  -- We can add hypotheses to a proof
+  addhyp⊢ : Γ ∈* Γ' → Γ ⊢ A → Γ' ⊢ A
+  addhyp⊢ s (zero x) = zero (mon∈∈* x s)
+  addhyp⊢ s (lam h) = lam (addhyp⊢ (both∈* s) h)
+  addhyp⊢ s (app h h₁) = app (addhyp⊢ s h) (addhyp⊢ s h₁)
+  addhyp⊢ s (andi h₁ h₂) = andi (addhyp⊢ s h₁) (addhyp⊢ s h₂)
+  addhyp⊢ s (ande₁ h) = ande₁ (addhyp⊢ s h)
+  addhyp⊢ s (ande₂ h) = ande₂ (addhyp⊢ s h)
+  addhyp⊢ s (true) = true
+  addhyp⊢ s (∀i h) = ∀i (addhyp⊢ s h)
+  addhyp⊢ s (∀e h) = ∀e (addhyp⊢ s h)
+
+  -- Extension of ⊢ to contexts
+  _⊢⁺_ : Con → Con → Prop
+  Γ ⊢⁺ [] = ⊤
+  Γ ⊢⁺ (F ∷ Γ') = (Γ ⊢ F) ∧ (Γ ⊢⁺ Γ')
+  infix 5 _⊢⁺_
+
+  -- We show that the relation respects ∈*
+
+  mon∈*⊢⁺ : Γ' ∈* Γ → Γ ⊢⁺ Γ'
+  mon∈*⊢⁺ zero∈* = tt
+  mon∈*⊢⁺ (next∈* x h) = ⟨ (zero x) , (mon∈*⊢⁺ h) ⟩
+
+  -- The relation respects ⊆
+  mon⊆⊢⁺ : Γ' ⊆ Γ → Γ ⊢⁺ Γ'
+  mon⊆⊢⁺ h = mon∈*⊢⁺ (⊆→∈* h)
+
+  -- The relation is reflexive
+  refl⊢⁺ : Γ ⊢⁺ Γ
+  refl⊢⁺ {[]} = tt
+  refl⊢⁺ {x ∷ Γ} = ⟨ zero zero∈ , mon⊆⊢⁺ (next⊆ zero⊆) ⟩
+
+  -- We can add hypotheses to to a proof
+  addhyp⊢⁺ : Γ ∈* Γ' → Γ ⊢⁺ Γ'' → Γ' ⊢⁺ Γ''
+  addhyp⊢⁺ {Γ'' = []} s h = tt
+  addhyp⊢⁺ {Γ'' = x ∷ Γ''} s ⟨ Γx , ΓΓ'' ⟩ = ⟨ addhyp⊢ s Γx , addhyp⊢⁺ s ΓΓ'' ⟩
+  
+  -- The relation respects ⊢
+  halftran⊢⁺ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺ Γ' → Γ' ⊢ F → Γ ⊢ F
+  halftran⊢⁺ {Γ' = F ∷ Γ'} h⁺ (zero zero∈) = proj₁ h⁺
+  halftran⊢⁺ {Γ' = F ∷ Γ'} h⁺ (zero (next∈ x)) = halftran⊢⁺ (proj₂ h⁺) (zero x)
+  halftran⊢⁺ h⁺ (lam h) = lam (halftran⊢⁺ ⟨ (zero zero∈) , (addhyp⊢⁺ (right∈* refl∈*) h⁺) ⟩ h)
+  halftran⊢⁺ h⁺ (app h h₁) = app (halftran⊢⁺ h⁺ h) (halftran⊢⁺ h⁺ h₁)
+  halftran⊢⁺ h⁺ (andi hf hg) = andi (halftran⊢⁺ h⁺ hf) (halftran⊢⁺ h⁺ hg)
+  halftran⊢⁺ h⁺ (ande₁ hfg) = ande₁ (halftran⊢⁺ h⁺ hfg)
+  halftran⊢⁺ h⁺ (ande₂ hfg) = ande₂ (halftran⊢⁺ h⁺ hfg)
+  halftran⊢⁺ h⁺ (true) = true
+  halftran⊢⁺ h⁺ (∀i h) = ∀i (halftran⊢⁺ h⁺ h)
+  halftran⊢⁺ h⁺ (∀e h {t}) = ∀e (halftran⊢⁺ h⁺ h)
+
+  -- The relation is transitive
+  tran⊢⁺ : {Γ Γ' Γ'' : Con} → Γ ⊢⁺ Γ' → Γ' ⊢⁺ Γ'' → Γ ⊢⁺ Γ''
+  tran⊢⁺ {Γ'' = []} h h' = tt
+  tran⊢⁺ {Γ'' = x ∷ Γ*} h h' = ⟨ halftran⊢⁺ h (proj₁ h') , tran⊢⁺ h (proj₂ h') ⟩
+
+ 
+
+  {--- DEFINITIONS OF ⊢⁰ and ⊢* ---}
+
+  -- ⊢⁰ are neutral forms
+  -- ⊢* are normal forms
+  data _⊢⁰_ : Con → Form → Prop
+  data _⊢*_ : Con → Form → Prop
+  data _⊢⁰_ where
+    zero : A ∈ Γ → Γ ⊢⁰ A
+    app : Γ ⊢⁰ (A ⇒ B) → Γ ⊢* A → Γ ⊢⁰ B
+    ande₁ : Γ ⊢⁰ A ∧∧ B → Γ ⊢⁰ A
+    ande₂ : Γ ⊢⁰ A ∧∧ B → Γ ⊢⁰ B
+    ∀e : {F : Term → Form} → Γ ⊢⁰ (∀∀ F) → ( {t : Term} → Γ ⊢⁰ (F t) )
+  data _⊢*_ where
+    neu⁰ : Γ ⊢⁰ Rel r ts → Γ ⊢* Rel r ts
+    lam : (A ∷ Γ) ⊢* B → Γ ⊢* (A ⇒ B)
+    andi : Γ ⊢* A → Γ ⊢* B → Γ ⊢* (A ∧∧ B)
+    ∀i : {F : Term → Form} → ({t : Term} → Γ ⊢* F t) → Γ ⊢* ∀∀ F
+    true : Γ ⊢* ⊤⊤
+  infix 5 _⊢⁰_
+  infix 5 _⊢*_
+
+
+-- We can add hypotheses to a proof
+  addhyp⊢⁰ : Γ ∈* Γ' → Γ ⊢⁰ A → Γ' ⊢⁰ A
+  addhyp⊢* : Γ ∈* Γ' → Γ ⊢* A → Γ' ⊢* A
+  addhyp⊢⁰ s (zero x) = zero (mon∈∈* x s)
+  addhyp⊢⁰ s (app h h₁) = app (addhyp⊢⁰ s h) (addhyp⊢* s h₁)
+  addhyp⊢⁰ s (ande₁ h) = ande₁ (addhyp⊢⁰ s h)
+  addhyp⊢⁰ s (ande₂ h) = ande₂ (addhyp⊢⁰ s h)
+  addhyp⊢⁰ s (∀e h {t}) = ∀e (addhyp⊢⁰ s h) {t}
+  addhyp⊢* s (neu⁰ x) = neu⁰ (addhyp⊢⁰ s x)
+  addhyp⊢* s (lam h) = lam (addhyp⊢* (both∈* s) h)
+  addhyp⊢* s (andi h₁ h₂) = andi (addhyp⊢* s h₁) (addhyp⊢* s h₂)
+  addhyp⊢* s true = true
+  addhyp⊢* s (∀i h) = ∀i (addhyp⊢* s h)
+
+  -- Extension of ⊢⁰ to contexts
+  -- i.e. there is a neutral proof for any element
+  _⊢⁰⁺_ : Con → Con → Prop
+  Γ ⊢⁰⁺ [] = ⊤
+  Γ ⊢⁰⁺ (F ∷ Γ') = (Γ ⊢⁰ F) ∧ (Γ ⊢⁰⁺ Γ')
+  infix 5 _⊢⁰⁺_
+
+  -- The relation respects ∈*
+
+  mon∈*⊢⁰⁺ : Γ' ∈* Γ → Γ ⊢⁰⁺ Γ'
+  mon∈*⊢⁰⁺ zero∈* = tt
+  mon∈*⊢⁰⁺ (next∈* x h) = ⟨ (zero x) , (mon∈*⊢⁰⁺ h) ⟩
+
+  -- The relation respects ⊆
+  mon⊆⊢⁰⁺ : Γ' ⊆ Γ → Γ ⊢⁰⁺ Γ'
+  mon⊆⊢⁰⁺ h = mon∈*⊢⁰⁺ (⊆→∈* h)
+
+  -- This relation is reflexive
+  refl⊢⁰⁺ : Γ ⊢⁰⁺ Γ
+  refl⊢⁰⁺ {[]} = tt
+  refl⊢⁰⁺ {x ∷ Γ} = ⟨ zero zero∈ , mon⊆⊢⁰⁺ (next⊆ zero⊆) ⟩
+
+  -- A useful lemma, that we can add hypotheses 
+  addhyp⊢⁰⁺ : Γ ∈* Γ' → Γ ⊢⁰⁺ Γ'' → Γ' ⊢⁰⁺ Γ''
+  addhyp⊢⁰⁺ {Γ'' = []} s h = tt
+  addhyp⊢⁰⁺ {Γ'' = A ∷ Γ'} s ⟨ Γx , ΓΓ'' ⟩ = ⟨ addhyp⊢⁰ s Γx , addhyp⊢⁰⁺ s ΓΓ'' ⟩
+
+  -- The relation preserves ⊢⁰ and ⊢*
+  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 zero∈ , addhyp⊢⁰⁺ (right∈* refl∈*) h⁺ ⟩ h)
+  halftran⊢⁰⁺* h⁺ (andi h₁ h₂) = andi (halftran⊢⁰⁺* h⁺ h₁) (halftran⊢⁰⁺* h⁺ h₂)
+  halftran⊢⁰⁺* h⁺ true = true
+  halftran⊢⁰⁺* h⁺ (∀i h) = ∀i (halftran⊢⁰⁺* h⁺ h)
+  halftran⊢⁰⁺⁰ {Γ' = x ∷ Γ'} h⁺ (zero zero∈) = proj₁ h⁺
+  halftran⊢⁰⁺⁰ {Γ' = x ∷ Γ'} h⁺ (zero (next∈ h)) = halftran⊢⁰⁺⁰ (proj₂ h⁺) (zero h)
+  halftran⊢⁰⁺⁰ h⁺ (app h h') = app (halftran⊢⁰⁺⁰ h⁺ h) (halftran⊢⁰⁺* h⁺ h')
+  halftran⊢⁰⁺⁰ h⁺ (ande₁ h) = ande₁ (halftran⊢⁰⁺⁰ h⁺ h)
+  halftran⊢⁰⁺⁰ h⁺ (ande₂ h) = ande₂ (halftran⊢⁰⁺⁰ h⁺ h)
+  halftran⊢⁰⁺⁰ h⁺ (∀e h {t}) = ∀e (halftran⊢⁰⁺⁰ h⁺ h)
+
+  -- The relation is transitive
+  tran⊢⁰⁺ : {Γ Γ' Γ'' : Con} → Γ ⊢⁰⁺ Γ' → Γ' ⊢⁰⁺ Γ'' → Γ ⊢⁰⁺ Γ''
+  tran⊢⁰⁺ {Γ'' = []} h h' = tt
+  tran⊢⁰⁺ {Γ'' = x ∷ Γ} h h' = ⟨ halftran⊢⁰⁺⁰ h (proj₁ h') , tran⊢⁰⁺ h (proj₂ h') ⟩
+