simpa using ⟨a, h, ha'⟩
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
a : α
as : List α
h : a ∈ as
f : α → List α
a' : α
ha' : a' ∈ f a
⊢ a' ∈ as.bind f
no goals