Theorem: List.multimop_single (Logic/Modal/LogicSymbol.lean)

State before:
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p q : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
⊢ List.multimop i n [p] = [(mop i)^[n] p]
Tactic:
simp
State after:
no goals