Reimplement `Permutation.Propositional` in terms of `Permutation.Setoid`

[MatthewDaggitt]

Unlike other binary relations over lists, Data.List.Relation.Binary.Permutation.(Setoid/Propositional) are implemented separately which results in an awful lot of proof duplication. It also means that other modules (e.g. Subset) don't play nice when trying to transfer results from setoid equality to propositional equality. I've added the breaking tag as it remains to be seen if they can be unified in a backwards compatible manner.

[MatthewDaggitt]

Parameterise Homogeneous relation by extra relation Q with Pointwise R => Q then use it to instantiate with propositional equality.

[MatthewDaggitt]

Blocked by typed pattern synonyms: agda/agda#2069.