constructor
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ CanonicalFrame L ∈ 𝔽(Ax(L)) ∧ ∃ V, ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := V } p
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ CanonicalFrame L ∈ 𝔽(Ax(L))

case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ ∃ V, ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := V } p