apply (Prod.Lex.le_iff (i,j) (i + 1,k)).mpr $ Or.inl $ Nat.lt_succ_self i
case a
t : Th
Δ : Ctx
f g : Form
h₁ : f¦g ∈ lindenbaumExtension t Δ
i j : ℕ
h₂ : f¦g ∈ lindenbaumSequence t Δ (i, j)
k : ℕ := Encodable.encode (f, g)
⊢ (i, j) ≤ (i + 1, k)
no goals