intros a b h₁
t : Th
Δ : Ctx
i : ℕ
⊢ Monotone fun j => lindenbaumSequence t Δ (i, j)
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
⊢ (fun j => lindenbaumSequence t Δ (i, j)) a ≤ (fun j => lindenbaumSequence t Δ (i, j)) b