have : (𝓓)-Consistent (∅, {p}) := by
  simp only [Tableau.ParametricConsistent, Collection.not_mem_empty, imp_false, Set.mem_singleton_iff];
  rintro Γ Δ hΓ hΔ;
  by_contra hC;
  replace hΓ : Γ = [] := List.nil_iff.mpr hΓ;
  subst hΓ;
  have : 𝓓 ⊢! p := disj_allsame'! hΔ (hC ⨀ verum!);
  contradiction;
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ ¬CanonicalModel 𝓓 ⊧ p
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
⊢ ¬CanonicalModel 𝓓 ⊧ p