have l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁ := by 
  cases l₁
  case inl h₂ => exact Or.inl h₂
  case inr h₂ => exact Or.inr ⟨h₂, le_refl b₁⟩
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)