exact 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 ∈ prev
no goals