have lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1) := by
  intros f h₃
  unfold lindenbaumSequence
  split
  case h_1 _ heq | h_2 _ heq => injection heq; contradiction
  case h_3 i' j' heq =>
    injection heq with heq₁ heq₂
    injection heq₂ with heq₂
    have heq₃ : j = j' := heq₂
    rw [←heq₁, ←heq₃]
    change
      let prev := lindenbaumSequence t Δ (i, j);
      let l := (Denumerable.ofNat (Form × Form) j).fst;
      let r := (Denumerable.ofNat (Form × Form) j).snd;
      f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
    intros prev l r
    split
    case inl =>
      split
      case inl | inr => apply Or.inl h₃
    case inr => exact h₃
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ (i, j + 1) → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i, j + 1)
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ (i, j + 1) → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i, j + 1)