[Agda] map⊆

[Sergei Meshveliani]

People,
I program mapping the _⊆_ relation on lists:

  ...

  map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) → {xs ys : List C} →
                                          xs ⊆ ys → map f xs ⊆' map f ys

  map⊆ f fCong {xs} {ys} xs⊆ys {z} z∈f-xs =
       let
         (x , x∈≡xs , fx≈z) = counter-map f xs z z∈f-xs
         x∈xs    = ∈≡→∈ x∈≡xs
         x∈ys    = xs⊆ys x∈xs
         fx∈f-ys = map∈ f fCong x∈ys
       in
       cong₁∈' fx≈z fx∈f-ys

Here _≈_ and _≈'_ are of the two corresponding setoids.
This implementation uses 

 map∈ : (f : C → C')  → (f Preserves _≈_ ⟶ _≈'_) → {x : C} →
        {xs : List C} → x ∈ xs                   → f x ∈' map f xs 
 ,
 counter-map : (f : C → C') → (xs : List C) → (y : C') → y ∈' map f xs →
                                               ∃ \x → x ∈≡ xs × f x ≈' y
 ,
 cong₁∈' : {zs : List C'} → (\x → x ∈' zs) Respects _≈'_

-- which I implement in their turn.


And I wonder of whether all this is inventing a bicycle.
Can  map⊆  be expressed in a simpler way?
What Standard library has for all this?

Thanks,

------
Sergei