case inr h₂ =>
  apply False.elim
  have l₇ : f¦f ∈ ▲prev := ⟨prf₃⟩
  rw [l₅,l₆] at h₂
  exact h₂ l₇
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 ∈ prev
no goals