intro p V w
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
⊢ ∀ (a : Formula α), ValidOnFrame F (□(□a ⟶ a) ⟶ □a)
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ w ⊧ □(□p ⟶ p) ⟶ □p