have : (L)-Consistent ({~p}) := by
  simp [ParametricConsistent];
  intro Γ hΓ;
  by_contra hC;
  have : L ⊢! p := dne'! $ replace_imply_left_conj'! hΓ hC;
  contradiction;
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
⊢ ¬CanonicalModel L ⊧ p
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
this : (L)-Consistent {~p}
⊢ ¬CanonicalModel L ⊧ p