[ add ] improve/refactor proofs of `Data.Bool.ListAction.Properties`

[jamesmckinna]

OK, so I experimented with my proposed refactoring, and surprise surprise not all was plain sailing...

• Data.Bool.Properties doesn't export any (obvious!) definitions of ∧-monoid, ∨-monoid, so the ++-homo theorem isn't directly applicable... (groan) FIXED in [ add ] missing Monoids to Data.Bool.Properties #3017
• there is some more plumbing to do to ensure that foldr and foldMap id are appropriately correctly identified, so that the theorem, even if applicable, actually returns the correct result definitionally... (sigh) TODO in [ add ] Data.List.Base.foldMap and refactor #3026
• I must at some point have run of steam refactoring Permutation with the result that the appeal to foldr-commMonoid itself requires so much extraneous additional plumbing to apply... (bewilderment) TODO largely now fixed in [ add ] Data.List.Base.foldMap and refactor #3026

So I'll write a cut-down review, and then let's merge this as-is, and figure out the mess afterwards!

Originally posted by @jamesmckinna in #3005 (comment)

See also my latest comment on #2553 of which this should perhaps be seen as a subsidiary issue?