. exact lindenbaum_next_indexed_parametricConsistent hCon n (by intro p hp; exact lindenbaum_next_indexed_subset₁_of_lt hm.le $ hΓ p hp) hΔ;
case intro.intro.inl
α : 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 : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inl
α : 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 : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hmn : m = n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inr
α : 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 : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
case intro.intro.inr.inl
α : 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 : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hmn : m = n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inr
α : 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 : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'