[ fix #1354 ] Refactoring Permutation.Propositional

[gallais]

Still missing: CHANGELOG entries

[MatthewDaggitt]

Closing as we've decided that its better to wait for typed pattern synonyms to finally make an appearance.

[jamesmckinna]

Suggest re-opening this, as I seem to have got it to work with the pattern synonyms... using some ideas from #2317 and #2321 towards further unification, if someone can help me unify the two Permutation.*.Properties modules along the lines considered in #2317 ... incoming revised/streamlined/refactored/rebased commits shortly.

UPDATED: as with that more recent PR, will convert to DRAFT for now until ready to review.

[JacquesCarette]

Other than that one odd name (which seems to actually be something pre-existing), this is looking quite good.

[jamesmckinna]

So far all the heavy lifting was done years ago by @gallais so props to him.

But I think that my recent work on #2317 hopefully points the way to getting the Properties unified as well. If that succeeds, then most of the guff in Propositional disappears entirely, and with it, all/most of the angst about qualified import of refl... I hope. Fingers crossed!

UPDATED Lots of refactoring work on #2317 ahead of bringing it to bear on this PR. But first see #2333 as a more manageable first part of a roadmap detailed there.

[jamesmckinna]

Removing the milestone marker from this for the time being...