lemma for `map` for `⊆` as Subset

[mechvel]

lib-2.0 needs a proof for the following lemma.

map⊆ :  (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) → (map f) Preserves _⊆_ ⟶ _⊆'_

This means:
if (f : C → C') , (f Preserves _≈_ ⟶ _≈'_),
is a map between the carriers of two setoids that agrees with the two equalities, then it preserves the relation ⊆ of Subset.

A simlar lemma for Sublist is provided in Data.List.Relation.Binary.Sublist.Setoid.Properties.
And the suggested lemma could probably be in
Data.List.Relation.Binary.Subset.Setoid.Properties.