obtain ⟨v, hwv, hvw'⟩ := 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
w' : M.Frame.World
hww' : w ≺^[n + 1] w'
h : ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
⊢ Satisfies M w' p
case succ.mp.intro.intro
α : 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
w' : M.Frame.World
h : ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
v : M.Frame.World
hwv : w ≺ v
hvw' : RelItr (fun x x_1 => x ≺ x_1) n v w'
⊢ Satisfies M w' p