case left a₁ b₁ h₂ => 
  have l₁ : a₁ < i ∨ a₁ = i := Nat.lt_or_eq_of_le $ Nat.lt_succ.mp h₂
  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₁⟩
  have l₃ := (Prod.Lex.le_iff (a₁, b₁) (i,b₁)).mpr l₂
  have l₄ := @lindenbaumSequenceMonotone' t Δ (i,b₁) (a₁, b₁) l₃
  apply le_trans l₄
  intros f h₂
  exact ⟨b₁,h₂⟩
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
no goals