case inl =>
  split
  case inl | inr => apply Or.inl h₃
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝ : l¦r ∈ ▲prev
⊢ f ∈ if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r}
no goals