import Mathlib
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix

namespace Syntax

inductive Tm : Type where
  | var : ℕ → Tm
  | and : Tm → Tm → Tm
  | or  : Tm → Tm → Tm
  | imp :  Tm → Tm → Tm
  | tt  : Tm
  | ff  : Tm

open Tm

scoped infixr:35 " ∧ " => Tm.and

scoped infixr:30 " ∨ " => Tm.or

scoped infixr:25 " ⇒ " => Tm.imp

abbrev Ctxt := List Tm

instance : LE Ctxt := ⟨(· <:+ ·)⟩

instance : Preorder Ctxt where
  le := (· <:+ ·)
  le_refl := fun _ => List.suffix_rfl
  le_trans := fun _ _ _ => List.IsSuffix.trans

inductive Pf : (Γ : Ctxt) → Tm → Prop where
  | assume : ∀ {Γ : Ctxt} {P : Tm} , Pf (P :: Γ ) P
  | wk : ∀ {Γ Δ : Ctxt} {P : Tm}, Γ ≤ Δ → Pf Γ P → Pf Δ P
  | and_I : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ P → Pf Γ Q → Pf Γ (P ∧ Q)
  | and_E₁ : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ (P ∧ Q) → Pf Γ P
  | and_E₂ : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ (P ∧ Q) → Pf Γ Q

  | or_I₁ : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ P → Pf Γ (P ∨ Q)
  | or_I₂ : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ Q → Pf Γ (P ∨ Q)
  | or_E  : ∀ {Γ : Ctxt} {P Q C : Tm}, Pf Γ (P ∨ Q) → Pf (P :: Γ) C → Pf (Q :: Γ) C → Pf Γ C
  | imp_I :  ∀ {Γ : Ctxt} {P Q : Tm}, Pf (P :: Γ) Q → Pf Γ (P ⇒ Q)
  | imp_E :  ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ (P ⇒ Q) → Pf Γ P → Pf Γ Q
  | ff_E  : ∀ {Γ : Ctxt}{P : Tm}, Pf Γ ff → Pf Γ P
  | tt_I :  ∀ {Γ : Ctxt}, Pf Γ tt

def example1 : Pf [] ((var 0 ⇒ var 1) ∧ var 0 ⇒ var 1) := by
⊢ Pf [] ((var 0 ⇒ var 1) ∧ var 0 ⇒ var 1)
  apply Pf.imp_I
a
⊢ Pf [(var 0 ⇒ var 1) ∧ var 0] (var 1)
  apply Pf.imp_E
a.a
⊢ Pf [(var 0 ⇒ var 1) ∧ var 0] (?a.P✝ ⇒ var 1)
a.a
⊢ Pf [(var 0 ⇒ var 1) ∧ var 0] ?a.P✝
a.P
⊢ Tm
  ·
a.a
⊢ Pf [(var 0 ⇒ var 1) ∧ var 0] (?a.P✝ ⇒ var 1) apply Pf.and_E₁
a.a.a
⊢ Pf [(var 0 ⇒ var 1) ∧ var 0] ((?a.P✝ ⇒ var 1) ∧ ?a.a.Q✝)
a.a.Q
⊢ Tm
    apply Pf.assume
  ·
a.a
⊢ Pf [(var 0 ⇒ var 1) ∧ var 0] ?a.P✝ apply Pf.and_E₂
a.a.a
⊢ Pf [(var 0 ⇒ var 1) ∧ var 0] (?a.a.P✝ ∧ var 0)
a.a.P
⊢ Tm
    apply Pf.assume

lemma cut {tm₂ : Tm} (tm₁ : Tm)
   (A : Pf Γ tm₁) (B : Pf (tm₁ :: Γ) tm₂) : Pf Γ tm₂ := by
Γ : Ctxt
tm₂ : Tm
tm₁ : Tm
A : Pf Γ tm₁
B : Pf (tm₁ :: Γ) tm₂
⊢ Pf Γ tm₂
  have B' : Pf Γ (tm₁ ⇒ tm₂) := by
Γ : Ctxt
tm₂ : Tm
tm₁ : Tm
A : Pf Γ tm₁
B : Pf (tm₁ :: Γ) tm₂
⊢ Pf Γ tm₂
    apply Pf.imp_I
a
Γ : Ctxt
tm₂ : Tm
tm₁ : Tm
A : Pf Γ tm₁
B : Pf (tm₁ :: Γ) tm₂
⊢ Pf (tm₁ :: Γ) tm₂; assumption
  apply Pf.imp_E B'
Γ : Ctxt
tm₂ : Tm
tm₁ : Tm
A : Pf Γ tm₁
B : Pf (tm₁ :: Γ) tm₂
B' : Pf Γ (tm₁ ⇒ tm₂)
⊢ Pf Γ tm₁
  assumption

namespace Pf

theorem of_mem {Γ : Ctxt} {P : Tm} (h : P ∈ Γ) : Pf Γ P := by
Γ : Ctxt
P : Tm
h : P ∈ Γ
⊢ Pf Γ P
  induction Γ with
  | nil =>
nil
P : Tm
h : P ∈ []
⊢ Pf [] P
      cases h
  | cons Q Γ ih =>
cons
P : Tm
Q : Tm
Γ : List Tm
ih : P ∈ Γ → Pf Γ P
h : P ∈ Q :: Γ
⊢ Pf (Q :: Γ) P
      simp at h
cons
P : Tm
Q : Tm
Γ : List Tm
ih : P ∈ Γ → Pf Γ P
h : P = Q ∨ P ∈ Γ
⊢ Pf (Q :: Γ) P
      rcases h with rfl | h
cons.inl
P : Tm
Γ : List Tm
ih : P ∈ Γ → Pf Γ P
⊢ Pf (P :: Γ) P
cons.inr
P : Tm
Q : Tm
Γ : List Tm
ih : P ∈ Γ → Pf Γ P
h : P ∈ Γ
⊢ Pf (Q :: Γ) P
      ·
cons.inl
P : Tm
Γ : List Tm
ih : P ∈ Γ → Pf Γ P
⊢ Pf (P :: Γ) P exact Pf.assume
      ·
cons.inr
P : Tm
Q : Tm
Γ : List Tm
ih : P ∈ Γ → Pf Γ P
h : P ∈ Γ
⊢ Pf (Q :: Γ) P exact Pf.wk (List.suffix_cons Q Γ) (ih h)

lemma quodlibet (φ t : Tm) : Pf [φ ⇒ Tm.ff] (φ ⇒ t) := by
φ : Tm
t : Tm
⊢ Pf [φ ⇒ ff] (φ ⇒ t)
  apply Pf.imp_I
a
φ : Tm
t : Tm
⊢ Pf [φ, φ ⇒ ff] t
  apply Pf.ff_E
a.a
φ : Tm
t : Tm
⊢ Pf [φ, φ ⇒ ff] ff
  apply Pf.imp_E
a.a.a
φ : Tm
t : Tm
⊢ Pf [φ, φ ⇒ ff] (?a.a.P✝ ⇒ ff)
a.a.a
φ : Tm
t : Tm
⊢ Pf [φ, φ ⇒ ff] ?a.a.P✝
a.a.P
φ : Tm
t : Tm
⊢ Tm
  ·
a.a.a
φ : Tm
t : Tm
⊢ Pf [φ, φ ⇒ ff] (?a.a.P✝ ⇒ ff) have hmem : (φ ⇒ Tm.ff) ∈ [φ, φ ⇒ Tm.ff] := by
φ : Tm
t : Tm
⊢ Pf [φ ⇒ ff] (φ ⇒ t) simp
    apply of_mem hmem
  ·
a.a.a
φ : Tm
t : Tm
⊢ Pf [φ, φ ⇒ ff] ?a.a.P✝ exact Pf.assume

lemma or_cases_to (φ ψ A : Tm) : Pf [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A := by
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A
  apply Pf.or_E
a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] (?P ∨ ?Q)
a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [?P, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A
a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [?Q, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A
P
φ : Tm
ψ : Tm
A : Tm
⊢ Tm
Q
φ : Tm
ψ : Tm
A : Tm
⊢ Tm
  ·
a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] (?P ∨ ?Q) have hmem : (φ ∨ ψ) ∈ [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] := by
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A simp
    exact Pf.of_mem hmem
  ·
a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [?P, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A apply Pf.imp_E
a.a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [φ, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] (?a.P✝ ⇒ A)
a.a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [φ, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] ?a.P✝
a.P
φ : Tm
ψ : Tm
A : Tm
⊢ Tm
    ·
a.a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [φ, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] (?a.P✝ ⇒ A) have hmem : (φ ⇒ A) ∈ [φ, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] := by
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A simp
      exact Pf.of_mem hmem
    ·
a.a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [φ, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] ?a.P✝ exact Pf.assume
  ·
a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [?Q, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A apply Pf.imp_E
a.a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [ψ, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] (?a.P✝ ⇒ A)
a.a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [ψ, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] ?a.P✝
a.P
φ : Tm
ψ : Tm
A : Tm
⊢ Tm
    ·
a.a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [ψ, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] (?a.P✝ ⇒ A) have hmem : (ψ ⇒ A) ∈ [ψ, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] := by
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A simp
      exact Pf.of_mem hmem
    ·
a.a
φ : Tm
ψ : Tm
A : Tm
⊢ Pf [ψ, φ ∨ ψ, φ ⇒ A, ψ ⇒ A] ?a.P✝ exact Pf.assume

theorem multicut {Δ : Ctxt} {P : Tm} (h : Pf Δ P) :
    ∀ {Γ : Ctxt}, (∀ Q ∈ Δ, Pf Γ Q) → Pf Γ P := by
Δ : Ctxt
P : Tm
h : Pf Δ P
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Δ, Pf Γ Q) → Pf Γ P
  induction h with
  | assume =>
assume
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ P✝
      intro Γ hΓ
assume
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Γ : Ctxt
hΓ : ∀ Q ∈ P✝ :: Γ✝, Pf Γ Q
⊢ Pf Γ P✝
      exact hΓ _ (by
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Γ : Ctxt
hΓ : ∀ Q ∈ P✝ :: Γ✝, Pf Γ Q
⊢ P✝ ∈ P✝ :: Γ✝ simp)
  | wk hΔ hP ih =>
wk
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
Δ✝ : Ctxt
P✝ : Tm
hΔ : Γ✝ ≤ Δ✝
hP : Pf Γ✝ P✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Δ✝, Pf Γ Q) → Pf Γ P✝
      intro Γ hΓ
wk
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
Δ✝ : Ctxt
P✝ : Tm
hΔ : Γ✝ ≤ Δ✝
hP : Pf Γ✝ P✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
Γ : Ctxt
hΓ : ∀ Q ∈ Δ✝, Pf Γ Q
⊢ Pf Γ P✝
      apply ih
wk.a
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
Δ✝ : Ctxt
P✝ : Tm
hΔ : Γ✝ ≤ Δ✝
hP : Pf Γ✝ P✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
Γ : Ctxt
hΓ : ∀ Q ∈ Δ✝, Pf Γ Q
⊢ ∀ Q ∈ Γ✝, Pf Γ Q
      intro Q hQ
wk.a
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
Δ✝ : Ctxt
P✝ : Tm
hΔ : Γ✝ ≤ Δ✝
hP : Pf Γ✝ P✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
Γ : Ctxt
hΓ : ∀ Q ∈ Δ✝, Pf Γ Q
Q : Tm
hQ : Q ∈ Γ✝
⊢ Pf Γ Q
      exact hΓ Q (hΔ.sublist.subset hQ)
  | and_I hP hQ ihP ihQ =>
and_I
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hP : Pf Γ✝ P✝
hQ : Pf Γ✝ Q✝
ihP : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
ihQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ Q✝
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∧ Q✝)
      intro Γ hΓ
and_I
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hP : Pf Γ✝ P✝
hQ : Pf Γ✝ Q✝
ihP : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
ihQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ Q✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
⊢ Pf Γ (P✝ ∧ Q✝)
      exact Pf.and_I (ihP hΓ) (ihQ hΓ)
  | and_E₁ hPQ ih =>
and_E₁
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf Γ✝ (P✝ ∧ Q✝)
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∧ Q✝)
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
      intro Γ hΓ
and_E₁
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf Γ✝ (P✝ ∧ Q✝)
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∧ Q✝)
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
⊢ Pf Γ P✝
      exact Pf.and_E₁ (ih hΓ)
  | and_E₂ hPQ ih =>
and_E₂
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf Γ✝ (P✝ ∧ Q✝)
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∧ Q✝)
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ Q✝
      intro Γ hΓ
and_E₂
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf Γ✝ (P✝ ∧ Q✝)
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∧ Q✝)
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
⊢ Pf Γ Q✝
      exact Pf.and_E₂ (ih hΓ)
  | or_I₁ hP ih =>
or_I₁
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hP : Pf Γ✝ P✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
      intro Γ hΓ
or_I₁
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hP : Pf Γ✝ P✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
⊢ Pf Γ (P✝ ∨ Q✝)
      exact Pf.or_I₁ (ih hΓ)
  | or_I₂ hQ ih =>
or_I₂
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hQ : Pf Γ✝ Q✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ Q✝
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
      intro Γ hΓ
or_I₂
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hQ : Pf Γ✝ Q✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ Q✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
⊢ Pf Γ (P✝ ∨ Q✝)
      exact Pf.or_I₂ (ih hΓ)
  | or_E hPQ hPC hQC ihPQ ihPC ihQC =>
or_E
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
C✝ : Tm
hPQ : Pf Γ✝ (P✝ ∨ Q✝)
hPC : Pf (P✝ :: Γ✝) C✝
hQC : Pf (Q✝ :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ C✝
      intro Γ hΓ
or_E
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
C✝ : Tm
hPQ : Pf Γ✝ (P✝ ∨ Q✝)
hPC : Pf (P✝ :: Γ✝) C✝
hQC : Pf (Q✝ :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
⊢ Pf Γ C✝
      exact Pf.or_E (ihPQ hΓ)
        (ihPC (Γ := _ :: Γ) (fun R hR => by
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
C✝ : Tm
hPQ : Pf Γ✝ (P✝ ∨ Q✝)
hPC : Pf (P✝ :: Γ✝) C✝
hQC : Pf (Q✝ :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R ∈ P✝ :: Γ✝
⊢ Pf (P✝ :: Γ) R
          simp at hR
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
C✝ : Tm
hPQ : Pf Γ✝ (P✝ ∨ Q✝)
hPC : Pf (P✝ :: Γ✝) C✝
hQC : Pf (Q✝ :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R = P✝ ∨ R ∈ Γ✝
⊢ Pf (P✝ :: Γ) R
          rcases hR with rfl | hR
inl
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
Q✝ : Tm
C✝ : Tm
hQC : Pf (Q✝ :: Γ✝) C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hPQ : Pf Γ✝ (R ∨ Q✝)
hPC : Pf (R :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (R ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ R :: Γ✝, Pf Γ Q) → Pf Γ C✝
⊢ Pf (R :: Γ) R
inr
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
C✝ : Tm
hPQ : Pf Γ✝ (P✝ ∨ Q✝)
hPC : Pf (P✝ :: Γ✝) C✝
hQC : Pf (Q✝ :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R ∈ Γ✝
⊢ Pf (P✝ :: Γ) R
          ·
inl
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
Q✝ : Tm
C✝ : Tm
hQC : Pf (Q✝ :: Γ✝) C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hPQ : Pf Γ✝ (R ∨ Q✝)
hPC : Pf (R :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (R ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ R :: Γ✝, Pf Γ Q) → Pf Γ C✝
⊢ Pf (R :: Γ) R exact Pf.assume
          ·
inr
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
C✝ : Tm
hPQ : Pf Γ✝ (P✝ ∨ Q✝)
hPC : Pf (P✝ :: Γ✝) C✝
hQC : Pf (Q✝ :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R ∈ Γ✝
⊢ Pf (P✝ :: Γ) R exact Pf.wk (List.suffix_cons _ Γ) (hΓ R hR)))
        (ihQC (Γ := _ :: Γ) (fun R hR => by
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
C✝ : Tm
hPQ : Pf Γ✝ (P✝ ∨ Q✝)
hPC : Pf (P✝ :: Γ✝) C✝
hQC : Pf (Q✝ :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R ∈ Q✝ :: Γ✝
⊢ Pf (Q✝ :: Γ) R
          simp at hR
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
C✝ : Tm
hPQ : Pf Γ✝ (P✝ ∨ Q✝)
hPC : Pf (P✝ :: Γ✝) C✝
hQC : Pf (Q✝ :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R = Q✝ ∨ R ∈ Γ✝
⊢ Pf (Q✝ :: Γ) R
          rcases hR with rfl | hR
inl
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
C✝ : Tm
hPC : Pf (P✝ :: Γ✝) C✝
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hPQ : Pf Γ✝ (P✝ ∨ R)
hQC : Pf (R :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ R)
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ R :: Γ✝, Pf Γ Q) → Pf Γ C✝
⊢ Pf (R :: Γ) R
inr
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
C✝ : Tm
hPQ : Pf Γ✝ (P✝ ∨ Q✝)
hPC : Pf (P✝ :: Γ✝) C✝
hQC : Pf (Q✝ :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R ∈ Γ✝
⊢ Pf (Q✝ :: Γ) R
          ·
inl
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
C✝ : Tm
hPC : Pf (P✝ :: Γ✝) C✝
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hPQ : Pf Γ✝ (P✝ ∨ R)
hQC : Pf (R :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ R)
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ R :: Γ✝, Pf Γ Q) → Pf Γ C✝
⊢ Pf (R :: Γ) R exact Pf.assume
          ·
inr
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
C✝ : Tm
hPQ : Pf Γ✝ (P✝ ∨ Q✝)
hPC : Pf (P✝ :: Γ✝) C✝
hQC : Pf (Q✝ :: Γ✝) C✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ∨ Q✝)
ihPC : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
ihQC : ∀ {Γ : Ctxt}, (∀ Q ∈ Q✝ :: Γ✝, Pf Γ Q) → Pf Γ C✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R ∈ Γ✝
⊢ Pf (Q✝ :: Γ) R exact Pf.wk (List.suffix_cons _ Γ) (hΓ R hR)))
  | imp_I hPQ ih =>
imp_I
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf (P✝ :: Γ✝) Q✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ Q✝
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ⇒ Q✝)
      intro Γ hΓ
imp_I
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf (P✝ :: Γ✝) Q✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ Q✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
⊢ Pf Γ (P✝ ⇒ Q✝)
      exact Pf.imp_I (ih (Γ := _ :: Γ) (fun R hR => by
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf (P✝ :: Γ✝) Q✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ Q✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R ∈ P✝ :: Γ✝
⊢ Pf (P✝ :: Γ) R
        simp at hR
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf (P✝ :: Γ✝) Q✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ Q✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R = P✝ ∨ R ∈ Γ✝
⊢ Pf (P✝ :: Γ) R
        rcases hR with rfl | hR
inl
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
Q✝ : Tm
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hPQ : Pf (R :: Γ✝) Q✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ R :: Γ✝, Pf Γ Q) → Pf Γ Q✝
⊢ Pf (R :: Γ) R
inr
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf (P✝ :: Γ✝) Q✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ Q✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R ∈ Γ✝
⊢ Pf (P✝ :: Γ) R
        ·
inl
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
Q✝ : Tm
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hPQ : Pf (R :: Γ✝) Q✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ R :: Γ✝, Pf Γ Q) → Pf Γ Q✝
⊢ Pf (R :: Γ) R exact Pf.assume
        ·
inr
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf (P✝ :: Γ✝) Q✝
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ P✝ :: Γ✝, Pf Γ Q) → Pf Γ Q✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
R : Tm
hR : R ∈ Γ✝
⊢ Pf (P✝ :: Γ) R exact Pf.wk (List.suffix_cons _ Γ) (hΓ R hR)))
  | imp_E hPQ hP ihPQ ihP =>
imp_E
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf Γ✝ (P✝ ⇒ Q✝)
hP : Pf Γ✝ P✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ⇒ Q✝)
ihP : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ Q✝
      intro Γ hΓ
imp_E
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
Q✝ : Tm
hPQ : Pf Γ✝ (P✝ ⇒ Q✝)
hP : Pf Γ✝ P✝
ihPQ : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ (P✝ ⇒ Q✝)
ihP : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
⊢ Pf Γ Q✝
      exact Pf.imp_E (ihPQ hΓ) (ihP hΓ)
  | ff_E hff ih =>
ff_E
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
hff : Pf Γ✝ ff
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ ff
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ P✝
      intro Γ hΓ
ff_E
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
P✝ : Tm
hff : Pf Γ✝ ff
ih : ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ ff
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
⊢ Pf Γ P✝
      exact Pf.ff_E (ih hΓ)
  | tt_I =>
tt_I
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
⊢ ∀ {Γ : Ctxt}, (∀ Q ∈ Γ✝, Pf Γ Q) → Pf Γ tt
      intro Γ hΓ
tt_I
Δ : Ctxt
P : Tm
Γ✝ : Ctxt
Γ : Ctxt
hΓ : ∀ Q ∈ Γ✝, Pf Γ Q
⊢ Pf Γ tt
      exact Pf.tt_I