induction n generalizing w with
| zero => simp;
| succ n ih =>
  constructor;
  . intro h w' hww';
    simp at h;
    obtain ⟨v, hwv, hvw'⟩ := hww';
    exact (ih.mp $ h _ hwv) w' hvw';
  . simp;
    intro h w' hww';
    apply ih.mpr;
    intro v hwv;
    exact h v w' hww' hwv;
α : Type u_1
M : Model α
w : M.World
p q : Formula α
n : ℕ
⊢ Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
no goals