simp [Kripke.ValidOnModel]
case mp.intro
α : 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}
Ω : MCT L
hΩ : {~p} ⊆ Ω.theory
⊢ ¬CanonicalModel L ⊧ p
case mp.intro
α : 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}
Ω : MCT L
hΩ : {~p} ⊆ Ω.theory
⊢ ∃ x, ¬Kripke.Satisfies (CanonicalModel L) x p