[Agda] All P xs -> x in xs -> ..

[Nils Anders Danielsson]

On 2013-10-23 17:13, Sergei Meshveliani wrote:
> has Standard library something close to
>
>    all-P→Px :  ... (P Respects _≈_) → All P xs → x ∈ xs → P x
> ?

I don't think so. If _≈_ is _≡_, then you can use Data.List.All.lookup.

-- 
/NAD