[Agda] all-P ?

[Sergei Meshveliani]

People,

I program  

  open import Data.List.All as All using () 
                                   renaming ([] to []a; _∷_ to _∷a_)
  ... 
  all-P : {A : Set} {P : A → Set} (p : (x : A) → P x) → (xs : List A) →
                                                            All.All P xs
  all-P p []       = []a
  all-P p (x ∷ xs) = p x ∷a (all-P p xs)

and use it like in this example:
                                                                      
  record Item : Set where field val   : ℕ
                                val>0 : val > 0
  open Item

  foo : (its : List Item) → All.All (\i → val i > 0) its
  foo = all-P val>0

The idea is to apply  all-P  instead of a recursive implementation for
each new function instead of  val>0.

Am I missing something?
Can this be achieved in a simpler way than by  all-P ?
I thought of  All.map,  but it occurs that it does not fit.  
Has Standard library something like  all-P ?

Thanks,

------
Sergei