. contrapose;
  intro h;
  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;
  obtain ⟨t', ht'⟩ := lindenbaum this;
  simp [ValidOnModel.iff_models, ValidOnModel]
  existsi t';
  apply truthlemma.not.mpr;
  apply t'.not_mem₁_iff_mem₂.mpr;
  simp_all;
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ CanonicalModel 𝓓 ⊧ p → 𝓓 ⊢! p

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p