existsi x
case succ.mp.intro.intro.intro.intro
α : 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
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
case succ.mp.intro.intro.intro.intro
α : 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
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x ∧ Satisfies M x p