case' inr h₁ => apply Or.inr
case inl
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
⊢ f ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev

case inr
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h✝ : ¬▲(prev ∪ {f}) ∩ Δ = ∅
⊢ (f ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev) ∨
    g ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev
case inr
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ¬▲(prev ∪ {f}) ∩ Δ = ∅
⊢ g ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev

case inl
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
⊢ f ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev