case inl h₂ =>
  split
  . rw [l₅]; exact Or.inr rfl
  . rw [l₆]; exact Or.inr rfl
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
⊢ f ∈ if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r}
no goals