case left a₁ b₁ h₂ =>
    have l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j := Or.inl h₂
    have l₂ := (Prod.Lex.le_iff (a₁, b₁) (i,j)).mpr l₁
    have l₃ := @lindenbaumSequenceMonotone' t Δ (i,j) (a₁, b₁)  l₂
    apply le_trans l₃
    exact lem
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
no goals