. contrapose;
  intro h;
  have : (L)-Consistent ({~p}) := by
    simp [ParametricConsistent];
    intro Γ hΓ;
    by_contra hC;
    have : L ⊢! p := dne'! $ replace_imply_left_conj'! hΓ hC;
    contradiction;
  obtain ⟨Ω, hΩ⟩ := lindenbaum this;
  simp [Kripke.ValidOnModel];
  existsi Ω;
  exact truthlemma.not.mpr $ iff_mem_neg.mp (show ~p ∈ Ω.theory by simp_all);
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ CanonicalModel L ⊧ p → L ⊢! p

case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ L ⊢! p → CanonicalModel L ⊧ p
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ L ⊢! p → CanonicalModel L ⊧ p