existsi t'
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ∃ x, ¬Satisfies (CanonicalModel 𝓓) x p
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ¬Satisfies (CanonicalModel 𝓓) t' p