intro h w' hww'
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ Satisfies M w (□^[(n + 1)]p) → ∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : Satisfies M w (□^[(n + 1)]p)
w' : M.Frame.World
hww' : w ≺^[n + 1] w'
⊢ Satisfies M w' p