Add the `Setoid`al structure of a (free) `Monoid` on `List`

[jamesmckinna]

(Extracted from #2350)
Module Data.List.Relation.Binary.Equality defines the Setoid lifting of equality from a Setoid on A to one on List A.

But nowhere that I can find is the ++-[]-monoid bundle/structure etc. defined for this Setoid... so we should add it.

See this blob #2393 for one possible implementation.

Issues:

• where should this construction live?
• what else should be added along these lines?
• what other 'obvious' Setoid liftings are missing?

NB this comment seems never to have been acted upon cf. #568

[jamesmckinna]

Downstream breaking (?) refactoring(s) (v3.0 or hypothetical-rewrite?)

• Data.List.Properties.Setoid
• Data.List.Properties.Propositional
  ???