obtain ⟨m, hm⟩ := ih
case cons.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].2
p : Formula α
Γ : List (Formula α)
ih : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1
case cons.intro.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].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1