cong-map analogues and such for map-with-∈

[mechvel]

As Standard library has map-with-∈, probably, it also needs analogues of cong-map
(, map-compose, map-id, ... ?) for map-with-∈ for the pointwise equlaity on lists.
Say,

module _ {α α= β β=} {A : Setoid α α=} {A' : Setoid β β=} where
  ...
  map-with-∈-cong : ∀ xs → (f g : ∀ {x} → x ∈ xs → C') →
                                 (∀ {x} → (x∈xs : x ∈ xs) → f x∈xs ≈' g x∈xs) →
                                 map-with-∈ xs f  =p  map-with-∈ xs g,

  map-with-∈≗map : ∀ xs → (f : C → C') → map-with-∈ xs (\ {x} x∈xs → f x)  =p  map f xs

-- ?

analogues and such for `map-with-∈

[MatthewDaggitt]

Blocked by #155

[MatthewDaggitt]

Closed with d9400f1