simp only [Tableau.ParametricConsistent, Collection.not_mem_empty, imp_false, Set.mem_singleton_iff]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ (𝓓)-Consistent (∅, {p})
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ ∀ {Γ Δ : List (Formula α)}, (∀ (p : Formula α), p ∉ Γ) → (∀ p_1 ∈ Δ, p_1 = p) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'