obtain ⟨m, hΓ⟩ : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1 := by
  induction Γ with
  | nil => simp;
  | cons p Γ ih =>
    simp_all;
    obtain ⟨i, hi⟩ := hΓ.1;
    obtain ⟨m, hm⟩ := ih;
    use (i + m);
    constructor;
    . exact lindenbaum_next_indexed_subset₁_of_lt (by simp) hi;
    . intro q hq;
      exact lindenbaum_next_indexed_subset₁_of_lt (by simp) $ hm 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
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
case intro
α : 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
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'