Theorem: LO.Propositional.Superintuitionistic.unprovable_classical_of_exists_ClassicalValuation (Logic/Propositional/Superintuitionistic/Kripke/Classical.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : ∃ V, ¬V ⊧ p
⊢ 𝐂𝐥 ⊬! p
Tactic:
apply not_imp_not.mpr $ Kripke.sound!
State after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : ∃ V, ¬V ⊧ p
⊢ ¬𝔽(Ax(𝐂𝐥)) ⊧ p

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : ∃ V, ¬V ⊧ p
⊢ ¬𝔽(Ax(𝐂𝐥)) ⊧ p
Tactic:
apply notClassicalValid_of_exists_ClassicalValuation
State after:
case a
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : ∃ V, ¬V ⊧ p
⊢ ∃ V, ¬V ⊧ p

State before:
case a
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : ∃ V, ¬V ⊧ p
⊢ ∃ V, ¬V ⊧ p
Tactic:
assumption
State after:
no goals