[Agda] (All P) Respects =pointwise

[Sergei Meshveliani]

Dear Standard library developers,

Has Standard library something for this:

  cong-All-pointwise : ∀ {p} {P : C → Set p} → P Respects _≈_ →
                                               (All P) Respects _=l_
?

Here  _≈_  is of a Setoid,  C its Carrier,
_=l_ the pointwise equality on  List C. 

Does Standard library need such?

Regards,

------
Sergei