induction Δ with
| nil => simp;
| cons p Δ ih =>
  simp_all;
  obtain ⟨i, hi⟩ := hΔ.1;
  obtain ⟨n, hn⟩ := ih;
  use (i + n);
  constructor;
  . exact lindenbaum_next_indexed_subset₂_of_lt (by simp) hi;
  . intro q hq;
    exact lindenbaum_next_indexed_subset₂_of_lt (by simp) $ hn q hq;
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
no goals