have l₂ := (Prod.Lex.le_iff (i, a) (i,b)).mpr $ Or.inr ⟨rfl,h₁⟩
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
⊢ lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
l₂ : ↑toLex (i, a) ≤ ↑toLex (i, b)
⊢ lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)