intro Γ Δ hΓ hΔ
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ (𝓓)-Consistent t∞
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t∞.1
hΔ : ∀ p ∈ Δ, p ∈ t∞.2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'