. simpa;
case succ.mpr.left
α : 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 y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y

case succ.mpr.right
α : 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 y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
case succ.mpr.right
α : 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 y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)