contrapose
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
⊢ Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p)) → Satisfies { Frame := F, Valuation := V } w (□p)
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
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□p) → ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))