case right b₁ h₂ =>
  cases h₂
  case refl => intros _ h₁; assumption
  case step h₂ =>
    have l₁ : i < i ∨ i = i ∧ b₁ ≤ j := Or.inr ⟨rfl, h₂⟩
    have l₂ := (Prod.Lex.le_iff (i, b₁) (i,j)).mpr l₁
    have l₃ := @lindenbaumSequenceMonotone' t Δ (i,j) (i, 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)
b₁ : ℕ
h₂ : b₁ ≤ j + 1
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
no goals