[Agda] Converting All2 to All

[Dr. ERDI Gergo]

On Sat, 6 Jan 2018, Dr. ERDI Gergo wrote:

> 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

Of course there's a symmetric all₂₂ with (λ x y → P y)as well.