case refl => intros _ h₁; assumption
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
⊢ lindenbaumSequence t Δ (i, j + 1) ⊆ lindenbaumSequence t Δ (i, j + 1)
no goals