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

[Sergei Meshveliani]

People,
has Standard library something close to 

  all-P→Px :  ... (P Respects _≈_) → All P xs → x ∈ xs → P x
?

Thanks,

------
Sergei