[Agda] generic map-cong

[Sergei Meshveliani]

People,

has it sense to consider a generalization for 
 
   Relation.Binary.PropositionalEquality._≗_  and 
   Data.List.Properties.map-cong 
?

map-cong  is for  _≗_ (and _≡_).

And the suggested  gen-map-cong  is for certain  _≈∘_  and  
the pointwise equality _=l_ on lists.

I suspect that I am missing something of Standard library.
I consider

--------------------------------------------------------------
module OfMapsToSetoid {α β β=} (A : Set α) (S : Setoid β β=)
  where
  open Setoid S using (_≈_) renaming (Carrier to B)

  _≈∘_ :  Rel (A → B) _
  f ≈∘ g =  {x : A} → f x ≈ g x

  lSetoid = ListPoint.setoid S

  open Setoid lSetoid using () renaming (_≈_ to _=l_)
  
  gen-map-cong : {f g : A → B} → f ≈∘ g → (xs : List A) → 
                                          map f xs =l map g xs
   ...
-------------------------------------------------------------

May be some more reasonable statements will be possible for _≈∘_
(?).

Has Standard library something for _≈∘_ ?

Thanks,

------
Sergei