classical_logic.agda

open import Data.Nat using (ℕ ; zero ; suc ; _≤_; z≤n ; s≤s ; _≤?_)
open import Relation.Nullary using (Dec ; yes ; no)
open import Relation.Nullary.Decidable using (True ; toWitness)
open import Function using (id ; _∘_)
open import Data.List using (List ; [] ; _∷_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

infix 25 #ᵗ_
infix 25 #ᶠ_
infix 24 ¬_
infixl 23 _∧_
infixl 22 _∨_
infixr 21 _⇒_
infixl 20 _,_
infix 19 _∋_
infix 19 _#_
infix 18 _-→_

data Proposition : Set where
  ⊤ ⊥ : Proposition
  _∧_ _∨_ _⇒_ : Proposition → Proposition → Proposition
  ¬_ : Proposition → Proposition

pattern ∅ = []
pattern _,_ xs x = x ∷ xs

data _∋_ : List Proposition → Proposition → Set where
  here : ∀ { xs x }
    → (xs , x) ∋ x
  there : ∀ { xs x y }
    → xs ∋ x
    → (xs , y) ∋ x

length : List Proposition → ℕ
length ∅ = 0
length (rest , _) = suc (length rest)

lookup : ∀ { xs i } → suc i ≤ length xs → Proposition
lookup {_ , p} {zero} (s≤s z≤n) = p
lookup {rest , _} {suc i} (s≤s i≤l) = lookup i≤l

scoped : ∀ { xs i } → (p : suc i ≤ length xs) → xs ∋ (lookup p)
scoped {_ , p} {zero} (s≤s z≤n) = here
scoped {rest , _} {suc _} (s≤s s≤l) = there (scoped s≤l)

mutual
  data _,_⊢_true (Δ : List Proposition) (Γ : List Proposition) : Proposition → Set where
    trivial : Δ , Γ ⊢ ⊤ true
    reference : ∀ { ϕ }
      → Δ ∋ ϕ
      → Δ , Γ ⊢ ϕ true
    absurd : ∀ { ϕ }
      → Δ , (Γ , ϕ) ⊢#
      → Δ , Γ ⊢ ϕ true
    ∧-true : ∀ { ϕ₁ ϕ₂ }
      → Δ , Γ ⊢ ϕ₁ true
      → Δ , Γ ⊢ ϕ₂ true
      → Δ , Γ ⊢ ϕ₁ ∧ ϕ₂ true
    ∨-true₁ : ∀ { ϕ₁ ϕ₂ }
      → Δ , Γ ⊢ ϕ₁ true
      → Δ , Γ ⊢ ϕ₁ ∨ ϕ₂ true
    ∨-true₂ : ∀ { ϕ₁ ϕ₂ }
      → Δ , Γ ⊢ ϕ₂ true
      → Δ , Γ ⊢ ϕ₁ ∨ ϕ₂ true
    ¬-true : ∀ { ϕ }
      → Δ , Γ ⊢ ϕ false
      → Δ , Γ ⊢ ¬ ϕ true
    ⇒-true : ∀ { ϕ₁ ϕ₂ }
      → (Δ , ϕ₁) , Γ ⊢ ϕ₂ true
      → Δ , Γ ⊢ ϕ₁ ⇒ ϕ₂ true

  data _,_⊢_false (Δ : List Proposition) (Γ : List Proposition) : Proposition → Set where
    trivial : Δ , Γ ⊢ ⊥ false
    reference : ∀ { ϕ }
      → Γ ∋ ϕ
      → Δ , Γ ⊢ ϕ false
    absurd : ∀ { ϕ }
      → (Δ , ϕ) , Γ ⊢#
      → Δ , Γ ⊢ ϕ false
    ∧-false₁ : ∀ { ϕ₁ ϕ₂ }
      → Δ , Γ ⊢ ϕ₁ false
      → Δ , Γ ⊢ ϕ₁ ∧ ϕ₂ false
    ∧-false₂ : ∀ { ϕ₁ ϕ₂ }
      → Δ , Γ ⊢ ϕ₂ false
      → Δ , Γ ⊢ ϕ₁ ∧ ϕ₂ false
    ∨-false : ∀ { ϕ₁ ϕ₂ }
      → Δ , Γ ⊢ ϕ₁ false
      → Δ , Γ ⊢ ϕ₂ false
      → Δ , Γ ⊢ ϕ₁ ∨ ϕ₂ false
    ¬-false : ∀ { ϕ }
      → Δ , Γ ⊢ ϕ true
      → Δ , Γ ⊢ ¬ ϕ false
    ⇒-false : ∀ { ϕ₁ ϕ₂ }
      → Δ , Γ ⊢ ϕ₁ true
      → Δ , Γ ⊢ ϕ₂ false
      → Δ , Γ ⊢ ϕ₁ ⇒ ϕ₂ false

  data _,_⊢# (Δ : List Proposition) (Γ : List Proposition) : Set where
    _#_ : ∀ { ϕ }
      → Δ , Γ ⊢ ϕ true
      → Δ , Γ ⊢ ϕ false
      → Δ , Γ ⊢#

#ᵗ_ : ∀ { Δ Γ }
  → (i : ℕ)
  → { p : True (suc i ≤? length Δ) }
  → Δ , Γ ⊢ (lookup (toWitness p)) true
#ᵗ_ i {p} = reference (scoped (toWitness p))

#ᶠ_ : ∀ { Δ Γ }
  → (i : ℕ)
  → { p : True (suc i ≤? length Γ) }
  → Δ , Γ ⊢ (lookup (toWitness p)) false
#ᶠ_ i {p} = reference (scoped (toWitness p))

extension : ∀ { Δ Γ }
  → (∀ { ϕ }   → Δ     ∋ ϕ → Γ     ∋ ϕ)
  → (∀ { ϕ ψ } → Δ , ψ ∋ ϕ → Γ , ψ ∋ ϕ)
extension ρ here = here
extension ρ (there n) = there (ρ n)

mutual
  renameᵗ : ∀ { Δ Δ' Γ Γ' }
    → (∀ { ϕ } → Δ ∋ ϕ → Δ' ∋ ϕ)
    → (∀ { ϕ } → Γ ∋ ϕ → Γ' ∋ ϕ)
    → (∀ { ϕ } → Δ , Γ ⊢ ϕ true → Δ' , Γ' ⊢ ϕ true)
  renameᵗ ρ σ trivial = trivial
  renameᵗ ρ σ (reference i) = reference (ρ i)
  renameᵗ ρ σ (absurd c) = absurd (rename-# ρ (extension σ) c)
  renameᵗ ρ σ (∧-true l-true r-true) = ∧-true (renameᵗ ρ σ l-true) (renameᵗ ρ σ r-true)
  renameᵗ ρ σ (∨-true₁ l-true) = ∨-true₁ (renameᵗ ρ σ l-true)
  renameᵗ ρ σ (∨-true₂ r-true) = ∨-true₂ (renameᵗ ρ σ r-true)
  renameᵗ ρ σ (¬-true a-false) = ¬-true (renameᶠ ρ σ a-false)
  renameᵗ ρ σ (⇒-true a-true) = ⇒-true (renameᵗ (extension ρ) σ a-true)

  renameᶠ : ∀ { Δ Δ' Γ Γ' }
    → (∀ { ϕ } → Δ ∋ ϕ → Δ' ∋ ϕ)
    → (∀ { ϕ } → Γ ∋ ϕ → Γ' ∋ ϕ)
    → (∀ { ϕ } → Δ , Γ ⊢ ϕ false → Δ' , Γ' ⊢ ϕ false)
  renameᶠ ρ σ trivial = trivial
  renameᶠ ρ σ (reference i) = reference (σ i)
  renameᶠ ρ σ (absurd c) = absurd (rename-# (extension ρ) σ c)
  renameᶠ ρ σ (∨-false l-false r-false) = ∨-false (renameᶠ ρ σ l-false) (renameᶠ ρ σ r-false)
  renameᶠ ρ σ (∧-false₁ l-false) = ∧-false₁ (renameᶠ ρ σ l-false)
  renameᶠ ρ σ (∧-false₂ r-false) = ∧-false₂ (renameᶠ ρ σ r-false)
  renameᶠ ρ σ (¬-false a-true) = ¬-false (renameᵗ ρ σ a-true)
  renameᶠ ρ σ (⇒-false a-true b-false) = ⇒-false (renameᵗ ρ σ a-true) (renameᶠ ρ σ b-false)

  rename-# : ∀ { Δ Δ' Γ Γ' }
    → (∀ { ϕ } → Δ ∋ ϕ → Δ' ∋ ϕ)
    → (∀ { ϕ } → Γ ∋ ϕ → Γ' ∋ ϕ)
    → (Δ , Γ ⊢# → Δ' , Γ' ⊢#)
  rename-# ρ σ (a-true # a-false) = renameᵗ ρ σ a-true # renameᶠ ρ σ a-false

extend_mapᵗ : ∀ { Δ Δ' Γ }
  → (∀ { ϕ }   → Δ     ∋ ϕ →  Δ'      , Γ ⊢ ϕ true)
  → (∀ { ϕ ψ } → Δ , ψ ∋ ϕ → (Δ' , ψ) , Γ ⊢ ϕ true)
extend_mapᵗ ρ here = reference here
extend_mapᵗ ρ (there n) = renameᵗ there id (ρ n)

extend_mapᶠ : ∀ { Δ Γ Γ' }
  → (∀ { ϕ }   → Γ     ∋ ϕ → Δ ,  Γ'      ⊢ ϕ false)
  → (∀ { ϕ ψ } → Γ , ψ ∋ ϕ → Δ , (Γ' , ψ) ⊢ ϕ false)
extend_mapᶠ σ here = reference here
extend_mapᶠ σ (there n) = renameᶠ id there (σ n)

mutual
  substituteᵗ : ∀ { Δ Δ' Γ Γ' }
    → (∀ { ϕ } → Δ ∋ ϕ → Δ' , Γ' ⊢ ϕ true)
    → (∀ { ϕ } → Γ ∋ ϕ → Δ' , Γ' ⊢ ϕ false)
    → (∀ { ϕ } → Δ , Γ ⊢ ϕ true → Δ' , Γ' ⊢ ϕ true)
  substituteᵗ ρ σ trivial = trivial
  substituteᵗ ρ σ (reference n) = ρ n
  substituteᵗ ρ σ (absurd r) = absurd (substitute-# (renameᵗ id there ∘ ρ) (extend_mapᶠ σ) r)
  substituteᵗ ρ σ (∧-true ϕ-true ψ-true) = ∧-true (substituteᵗ ρ σ ϕ-true) (substituteᵗ ρ σ ψ-true)
  substituteᵗ ρ σ (∨-true₁ ϕ-true) = ∨-true₁ (substituteᵗ ρ σ ϕ-true)
  substituteᵗ ρ σ (∨-true₂ ψ-true) = ∨-true₂ (substituteᵗ ρ σ ψ-true)
  substituteᵗ ρ σ (¬-true ϕ-false) = ¬-true (substituteᶠ ρ σ ϕ-false)
  substituteᵗ ρ σ (⇒-true ϕ-true) = ⇒-true (substituteᵗ (extend_mapᵗ ρ) (renameᶠ there id ∘ σ) ϕ-true)

  substituteᶠ : ∀ { Δ Δ' Γ Γ' }
    → (∀ { ϕ } → Δ ∋ ϕ → Δ' , Γ' ⊢ ϕ true)
    → (∀ { ϕ } → Γ ∋ ϕ → Δ' , Γ' ⊢ ϕ false)
    → (∀ { ϕ } → Δ , Γ ⊢ ϕ false → Δ' , Γ' ⊢ ϕ false)
  substituteᶠ ρ σ trivial = trivial
  substituteᶠ ρ σ (reference n) = σ n
  substituteᶠ ρ σ (absurd r) = absurd (substitute-# (extend_mapᵗ ρ) (renameᶠ there id ∘ σ) r)
  substituteᶠ ρ σ (∧-false₁ ϕ-false) = ∧-false₁ (substituteᶠ ρ σ ϕ-false)
  substituteᶠ ρ σ (∧-false₂ ψ-false) = ∧-false₂ (substituteᶠ ρ σ ψ-false)
  substituteᶠ ρ σ (∨-false ϕ-false ψ-false) = ∨-false (substituteᶠ ρ σ ϕ-false) (substituteᶠ ρ σ ψ-false)
  substituteᶠ ρ σ (¬-false ϕ-true) = ¬-false (substituteᵗ ρ σ ϕ-true)
  substituteᶠ ρ σ (⇒-false ϕ-true ψ-false) = ⇒-false (substituteᵗ ρ σ ϕ-true) (substituteᶠ ρ σ ψ-false)

  substitute-# : ∀ { Δ Δ' Γ Γ' }
    → (∀ { ϕ } → Δ ∋ ϕ → Δ' , Γ' ⊢ ϕ true)
    → (∀ { ϕ } → Γ ∋ ϕ → Δ' , Γ' ⊢ ϕ false)
    → (Δ , Γ ⊢# → Δ' , Γ' ⊢#)
  substitute-# ρ σ (ϕ-true # ϕ-false) = substituteᵗ ρ σ ϕ-true # substituteᶠ ρ σ ϕ-false

_[_ᵗ]# : ∀ { Δ Γ ϕ }
  → (Δ , ϕ) , Γ ⊢#
  → Δ , Γ ⊢ ϕ true
  → Δ , Γ ⊢#
_[_ᵗ]# {Δ} {Γ} {ϕ} f x = substitute-# ρ reference f
  where
    ρ : ∀ { ψ } → (Δ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ true
    ρ here = x
    ρ (there n) = reference n

_[_ᶠ]# : ∀ { Δ Γ ϕ }
  → Δ , (Γ , ϕ) ⊢#
  → Δ , Γ ⊢ ϕ false
  → Δ , Γ ⊢#
_[_ᶠ]# {Δ} {Γ} {ϕ} f x = substitute-# reference σ f
  where
    σ : ∀ { ψ } → (Γ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ false
    σ here = x
    σ (there n) = reference n

_[_ᵗ]ᵗ : ∀ { Δ Γ ϕ ψ }
  → (Δ , ϕ) , Γ ⊢ ψ true
  → Δ , Γ ⊢ ϕ true
  → Δ , Γ ⊢ ψ true
_[_ᵗ]ᵗ {Δ} {Γ} {ϕ} f x = substituteᵗ ρ reference f
  where
    ρ : ∀ { ψ } → (Δ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ true
    ρ here = x
    ρ (there n) = reference n

_[_ᶠ]ᵗ : ∀ { Δ Γ ϕ ψ }
  → Δ , (Γ , ϕ) ⊢ ψ true
  → Δ , Γ ⊢ ϕ false
  → Δ , Γ ⊢ ψ true
_[_ᶠ]ᵗ {Δ} {Γ} {ϕ} f x = substituteᵗ reference σ f
  where
    σ : ∀ { ψ } → (Γ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ false
    σ here = x
    σ (there n) = reference n

_[_ᵗ]ᶠ : ∀ { Δ Γ ϕ ψ }
  → (Δ , ϕ) , Γ ⊢ ψ false
  → Δ , Γ ⊢ ϕ true
  → Δ , Γ ⊢ ψ false
_[_ᵗ]ᶠ {Δ} {Γ} {ϕ} f x = substituteᶠ ρ reference f
  where
    ρ : ∀ { ψ } → (Δ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ true
    ρ here = x
    ρ (there n) = reference n

_[_ᶠ]ᶠ : ∀ { Δ Γ ϕ ψ }
  → Δ , (Γ , ϕ) ⊢ ψ false
  → Δ , Γ ⊢ ϕ false
  → Δ , Γ ⊢ ψ false
_[_ᶠ]ᶠ {Δ} {Γ} {ϕ} f x = substituteᶠ reference σ f
  where
    σ : ∀ { ψ } → (Γ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ false
    σ here = x
    σ (there n) = reference n

data _-→_ { Δ Γ } : Δ , Γ ⊢# → Δ , Γ ⊢# → Set where
  ∧-→1 : ∀ { ϕ ψ } { ϕ-true : Δ , Γ ⊢ ϕ true } { ψ-true : Δ , Γ ⊢ ψ true } { ϕ-false : Δ , Γ ⊢ ϕ false }
    → ∧-true ϕ-true ψ-true # ∧-false₁ ϕ-false -→ ϕ-true # ϕ-false
  ∧-→2 : ∀ { ϕ ψ } { ϕ-true : Δ , Γ ⊢ ϕ true } { ψ-true : Δ , Γ ⊢ ψ true } { ψ-false : Δ , Γ ⊢ ψ false }
    → ∧-true ϕ-true ψ-true # ∧-false₂ ψ-false -→ ψ-true # ψ-false
  ∨-→1 : ∀ { ϕ ψ } { ϕ-true : Δ , Γ ⊢ ϕ true } { ϕ-false : Δ , Γ ⊢ ϕ false } { ψ-false : Δ , Γ ⊢ ψ false }
    → ∨-true₁ ϕ-true # ∨-false ϕ-false ψ-false -→ ϕ-true # ϕ-false
  ∨-→2 : ∀ { ϕ ψ } { ψ-true : Δ , Γ ⊢ ψ true } { ϕ-false : Δ , Γ ⊢ ϕ false } { ψ-false : Δ , Γ ⊢ ψ false }
    → ∨-true₂ ψ-true # ∨-false ϕ-false ψ-false -→ ψ-true # ψ-false
  ¬-→ : ∀ { ϕ } { ϕ-true : Δ , Γ ⊢ ϕ true } { ϕ-false : Δ , Γ ⊢ ϕ false }
    → ¬-true ϕ-false # ¬-false ϕ-true -→ ϕ-true # ϕ-false
  ⇒-→ : ∀ { ϕ ψ } { ϕ-true : Δ , Γ ⊢ ϕ true } { ψ-true : (Δ , ϕ) , Γ ⊢ ψ true } { ψ-false : Δ , Γ ⊢ ψ false }
    → ⇒-true ψ-true # ⇒-false ϕ-true ψ-false -→ ψ-true [ ϕ-true ᵗ]ᵗ # ψ-false
  absurdᵗ-→ : ∀ { ϕ ψ } { p : Δ , (Γ , ϕ) ⊢ ψ true } { k : Δ , (Γ , ϕ) ⊢ ψ false } { ϕ-false : Δ , Γ ⊢ ϕ false }
    → absurd (p # k) # ϕ-false -→ p [ ϕ-false ᶠ]ᵗ # k [ ϕ-false ᶠ]ᶠ
  absurdᶠ-→ : ∀ { ϕ ψ } { p : (Δ , ϕ) , Γ ⊢ ψ true } { k : (Δ , ϕ) , Γ ⊢ ψ false } { ϕ-true : Δ , Γ ⊢ ϕ true }
    → ϕ-true # absurd (p # k) -→ p [ ϕ-true ᵗ]ᵗ # k [ ϕ-true ᵗ]ᶠ

data _isPrefixOf_ : List Proposition → List Proposition → Set where
  refl : ∀ { Δ } → Δ isPrefixOf Δ
  weaken : ∀ { Δ Γ ϕ } → Δ isPrefixOf Γ → Δ isPrefixOf (Γ , ϕ)

∅-bottom : ∀ { Δ } → ∅ isPrefixOf Δ
∅-bottom {∅} = refl
∅-bottom {Δ , _} = weaken ∅-bottom

_isPrefixOf?_ : (Δ : List Proposition) → (Γ : List Proposition) → Dec (Δ isPrefixOf Γ)
_isPrefixOf?_ ∅ _ = yes ∅-bottom
_isPrefixOf?_ (Δ , _) ∅ = no λ()
_isPrefixOf?_ (Δ , ϕ) (Γ , ψ) with (Δ , ϕ) isPrefixOf? Γ
... | yes p = yes (weaken p)
... | no _ = {!!}

wow-such-logic : ∀ { Δ Γ ϕ ψ }
  → Δ , Γ ⊢ ϕ false
  → Δ , Γ ⊢ ϕ ⇒ ψ true
wow-such-logic ϕ-false = ⇒-true (absurd (#ᵗ 0 # renameᶠ there there ϕ-false))

ap : ∀ { Δ Γ ϕ ψ }
  → Δ , Γ ⊢ ϕ true
  → Δ , Γ ⊢ ϕ ⇒ ψ true
  → Δ , Γ ⊢ ψ true
ap ϕ-true ϕ⇒ψ-true = absurd (renameᵗ id there ϕ⇒ψ-true # ⇒-false (renameᵗ id there ϕ-true) (#ᶠ 0))

∧-true-elim₁ : ∀ { Δ Γ ϕ ψ }
  → Δ , Γ ⊢ ϕ ∧ ψ true
  → Δ , Γ ⊢ ϕ true
∧-true-elim₁ ϕ∧ψ-true = absurd (renameᵗ id there ϕ∧ψ-true # ∧-false₁ (#ᶠ 0))

∨-false-elim₁ : ∀ { Δ Γ ϕ ψ }
  → Δ , Γ ⊢ ϕ ∨ ψ false
  → Δ , Γ ⊢ ϕ false
∨-false-elim₁ ϕ∨ψ-false = absurd (∨-true₁ (#ᵗ 0) # renameᶠ there id ϕ∨ψ-false)

∨-false-elim₂ : ∀ { Δ Γ ϕ ψ }
  → Δ , Γ ⊢ ϕ ∨ ψ false
  → Δ , Γ ⊢ ψ false
∨-false-elim₂ ϕ∨ψ-false = absurd (∨-true₂ (#ᵗ 0) # renameᶠ there id ϕ∨ψ-false)

refl-true : ∀ { Δ Γ ϕ }
  → (Δ , ϕ) , Γ ⊢ ϕ true
refl-true = #ᵗ 0

deMorgan : ∀ { Δ Γ ϕ ψ }
  → Δ , Γ ⊢ ϕ ∨ ψ false
  → Δ , Γ ⊢ (¬ ϕ) ∧ (¬ ψ) true
deMorgan ϕ∧ψ-false = ∧-true (¬-true (∨-false-elim₁ ϕ∧ψ-false)) ((¬-true (∨-false-elim₂ ϕ∧ψ-false)))

¬¬-elimᵗ : ∀ { Δ Γ ϕ }
  → Δ , Γ ⊢ ¬ (¬ ϕ) true
  → Δ , Γ ⊢ ϕ true
¬¬-elimᵗ ¬¬ϕ-true = absurd (renameᵗ id there ¬¬ϕ-true # ¬-false (¬-true (#ᶠ 0)))

¬¬-elimᶠ : ∀ { Δ Γ ϕ }
  → Δ , Γ ⊢ ¬ (¬ ϕ) false
  → Δ , Γ ⊢ ϕ false
¬¬-elimᶠ ¬¬ϕ-false = absurd (¬-true (¬-false (#ᵗ 0)) # renameᶠ there id ¬¬ϕ-false)

¬-elimᵗ : ∀ { Δ Γ ϕ }
  → Δ , Γ ⊢ ¬ ϕ false
  → Δ , Γ ⊢ ϕ true
¬-elimᵗ = ¬¬-elimᵗ ∘ ¬-true

¬-elimᶠ : ∀ { Δ Γ ϕ }
  → Δ , Γ ⊢ ¬ ϕ true
  → Δ , Γ ⊢ ϕ false
¬-elimᶠ = ¬¬-elimᶠ ∘ ¬-false

contraposition : ∀ { Δ Γ ϕ ψ }
  → Δ , Γ ⊢ ϕ ⇒ ψ true
  → Δ , Γ ⊢ (¬ ψ) ⇒ (¬ ϕ) true
contraposition ϕ⇒ψ-true = ⇒-true (absurd (ap (¬-elimᵗ (#ᶠ 0)) (renameᵗ there there ϕ⇒ψ-true) # ¬-elimᶠ (#ᵗ 0)))

decontraposition : ∀ { Δ Γ ϕ ψ }
  → Δ , Γ ⊢ (¬ ψ) ⇒ (¬ ϕ) true
  → Δ , Γ ⊢ ϕ ⇒ ψ true
decontraposition ¬ψ⇒¬ϕ = ⇒-true (¬¬-elimᵗ (ap (¬-true (¬-false (#ᵗ 0))) (renameᵗ there id (contraposition ¬ψ⇒¬ϕ))))

∨-true-elim : ∀ { Δ Γ ϕ ψ ω }
  → Δ , Γ ⊢ ϕ ∨ ψ true
  → (Δ , ϕ) , Γ ⊢ ω true
  → (Δ , ψ) , Γ ⊢ ω true
  → Δ , Γ ⊢ ω true
∨-true-elim ϕ∨ψ-true f g = absurd (renameᵗ id there ϕ∨ψ-true # ∨-false (absurd (ap (#ᵗ 0) (renameᵗ there there (⇒-true f))# (#ᶠ 0)))
                                                                                         (absurd (ap (#ᵗ 0) (renameᵗ there there (⇒-true g)) # (#ᶠ 0))))

∧-false-elim : ∀ { Δ Γ ϕ ψ ω }
  → Δ , Γ ⊢ ϕ ∧ ψ false
  → Δ , (Γ , ϕ) ⊢ ω false
  → Δ , (Γ , ψ) ⊢ ω false
  → Δ , Γ ⊢ ω false
∧-false-elim ϕ∧ψ-false f g = absurd (∧-true (absurd ((#ᵗ 0) # {!!})) {!!} # renameᶠ there id ϕ∧ψ-false)

_ : ∀ { Δ Γ ϕ ψ θ }
  → Δ , Γ ⊢ (ϕ ∧ (ψ ∧ θ)) ⇒ (ϕ ∧ θ) true
_ = ⇒-true (absurd ((#ᵗ 0) # ∧-false₂ (∧-false₂ (absurd ((#ᵗ 1) # ∧-false₁ (absurd (∧-true (#ᵗ 0) (#ᵗ 1) # (#ᶠ 0))))))))