[Agda] pointwise congr.of ++

[Sergei Meshveliani]

People,

For the pointwise equality  _=l_  on  lists over any setoid  A,  
I program

  ++cong-=l :  _++_ Preserves₂ _=l_ ⟶ _=l_ ⟶ _=l_

Is this lemma in Standard library?

Thanks,

------
Sergei