exact ⟨loeb hp⟩
case intro
F : Type u_1
inst✝⁸ : StandardModalLogicalConnective F
inst✝⁷ : DecidableEq F
S : Type u_2
inst✝⁶ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁵ : Classical 𝓢
inst✝⁴ : System.NegationEquiv 𝓢
inst✝³ : Necessitation 𝓢
inst✝² inst✝¹ : HasAxiomK 𝓢
inst✝ : LoebRule 𝓢
hp : 𝓢 ⊢ □p ⟶ p
⊢ 𝓢 ⊢! p
no goals