Theorem: LO.UnaryModalOperator.multimop_succ (Logic/Modal/LogicSymbol.lean)

State before:
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ (mop i)^[n + 1] p = mop i ((mop i)^[n] p)
Tactic:
apply iterate_succ_apply'
State after:
no goals