simpa
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
h : ∀ p ∈ l, p ∈ Set.multimop i n s
q : F
left✝ : q ∈ s
hp : (mop i)^[n] q ∈ l
⊢ q ∈ s ∧ (mop i)^[n] q = (mop i)^[n] q
no goals