[Agda] Converting All2 to All

[Dr. ERDI Gergo]

I've written the following function for Data.Vect.All (but it would apply 
just the same for Data.List.All):

all₂₁ : ∀ {a b} {A : Set a} {B : Set b} {P : A → Set}
   {n} {xs : Vec A n} {ys : Vec B n} →
   All₂ (λ x y → P x) xs ys → All P xs
all₂₁ []        = []
all₂₁ (p ∷ ps)  = p ∷ all₂₁ ps

My questions are:
1. What would be a good name for this function? (I am fairly certain all₂₁ 
is not one:))
2. Should I add it to the stdlib?

Thanks,
 	Gergo