change (Denumerable.ofNat (Form × Form) k).snd = g
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
⊢ r = g
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
⊢ (Denumerable.ofNat (Form × Form) k).snd = g