. rw [l₅]; exact Or.inr rfl
case inl
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
h✝ : ▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {l}

case inr
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
h✝ : ¬▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {r}
case inr
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
h✝ : ¬▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {r}