apply Finset.toList_insert
ι : 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
hl : p ∉ l
⊢ (insert ((mop i)^[n] p) (Finset.image (mop i)^[n] l.toFinset)).toList ~
    (mop i)^[n] p :: (Finset.multimop i n l.toFinset).toList
case h
ι : 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
hl : p ∉ l
⊢ (mop i)^[n] p ∉ Finset.image (mop i)^[n] l.toFinset