simp_all
case cons
α : 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
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : (∀ p ∈ Δ, ∃ i, p ∈ t[i].2) → ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : ∀ p_1 ∈ p :: Δ, ∃ i, p_1 ∈ t[i].2
⊢ ∃ n, ∀ p_1 ∈ p :: Δ, p_1 ∈ t[n].2
case cons
α : 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
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2