decidable search on a list

Stream: Is there code for X?

[Bhavik Mehta]

instance (f : α → Prop) (l : list α) [decidable_pred f] : decidable (∃ a, a ∈ l ∧ f a) :=
begin

end

How can I get this to work without going classical? (In case this is #xy, my actual case is in defining an algorithm where I want to get something from the list if there is one, and doing nothing if there isn't one)

[Kenny Lau]

have you tried moving the membership to the existential clause?

[Bhavik Mehta]

that works but then when I try to use it, list.choose gets confused

[Kenny Lau]

well you can destruct the existential when providing the proof for list.choose

[Bhavik Mehta]

But this is a different problem so that works, thanks!