exact ⟨⟨t, hMax, hCon⟩, ht⟩
case intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t₀ : Tableau α
hCon✝ : (𝓓)-Consistent t₀
t : Tableau α
ht : t₀ ⊆ t
hCon : (𝓓)-Consistent t
hMax : t.Saturated
⊢ ∃ t, t₀ ⊆ t.tableau
no goals