simp
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ ∀ (x x_1 : M.Frame.World),
    w ≺ x_1 →
      RelItr (fun x x_2 => x ≺ x_2) n x_1 x →
        Satisfies M x p → ∃ w', w ≺ w' ∧ Satisfies M w' ((UnaryModalOperator.mop false)^[n] p)