case h_3 i' j' heq =>
  injection heq with heq₁ heq₂
  injection heq₂ with heq₂
  have heq₃ : j = j' := heq₂
  rw [←heq₁, ←heq₃]
  change
    let prev := lindenbaumSequence t Δ (i, j);
    let l := (Denumerable.ofNat (Form × Form) j).fst;
    let r := (Denumerable.ofNat (Form × Form) j).snd;
    f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
  intros prev l r
  split
  case inl =>
    split
    case inl | inr => apply Or.inl h₃
  case inr => exact h₃
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq : (i, j + 1) = (i', Nat.succ j')
⊢ f ∈
    let prev := lindenbaumSequence t Δ (i', j');
    let l := (Denumerable.ofNat (Form × Form) j').fst;
    let r := (Denumerable.ofNat (Form × Form) j').snd;
    if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
no goals