. simp;
  intro h w' hww';
  apply ih.mpr;
  intro v hwv;
  exact h v w' hww' hwv;
case succ.mpr
α : 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
⊢ (∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p) → Satisfies M w (□^[(n + 1)]p)
no goals