intro v 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
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ∀ (v : M.Frame.World), w' ≺^[n] v → Satisfies M v p
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
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
v : M.Frame.World
hwv : w' ≺^[n] v
⊢ Satisfies M v p