induction n generalizing w with
| zero => simp;
| succ n ih =>
  constructor;
  . intro h;
    obtain ⟨v, hwv, hv⟩ := by simpa using h;
    obtain ⟨x, hvx, hx⟩ := ih.mp hv;
    existsi x;
    constructor;
    . existsi v; simp_all;
    . simpa;
  . simp;
    intro x y hwy hyx hx;
    existsi y;
    constructor;
    . simpa;
    . apply ih.mpr;
      existsi x;
      simp_all;
α : Type u_1
M : Model α
w : M.World
p q : Formula α
n : ℕ
⊢ Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
no goals