subst hΓ
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
hΓ : Γ = []
⊢ False
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! [].conj' ⟶ Δ.disj'
⊢ False