[ refactor ] proofs under Data.List.Membership.*.Properties

[jamesmckinna]

This fixes the low-hanging-fruit item under issue #2542 concerning the switch to a postfix definition of:
_∉[] : (x : A) → x ∉ [] in each of

• Data.List.Membership.Setoid.Properties
• Data.List.Membership.Propositional.Properties.Core

Additionally:

• cleans up imports: resp rather than its equivalent subst;
• refactors to remove all uses of rewrite in the second module above, in the spirit of recent discussions.

UPDATED:

• most recent (knock-on) commit exposes a slight wrinkle in the parameterisation: use here of the lemma, instantiated to Setoid S arises there as (S Membershipₚ.∉[]) _ which looks... not quite right wrt the original problem (and removing parentheses causes a parse error!) but tweaked now to look a bit more reasonable?

[MatthewDaggitt]

Thanks @jamesmckinna !

[MatthewDaggitt]

most recent (knock-on) commit exposes a slight wrinkle in the parameterisation: use here of the lemma, instantiated to Setoid S arises there as (S Membershipₚ.∉[]) _ which looks... not quite right wrt the original problem (and removing parentheses causes a parse error!) but tweaked now to look a bit more reasonable?

This has just sunk in. Yes, this is why we don't use misfix proofs as a rule, because complex module parameterisations often screw them over, and the contents of the modules should be usable regardless of whether the module parameters are provided or not.

I'd vote for staying with the current policy of not using misfix for proofs therefore (and codifying it in the style guide?).... Sorry, this is my fault, I knew this many years ago, but no longer.

[jamesmckinna]

Thanks for the careful consideration @MatthewDaggitt !

So... I'll revert the controversial commits, but cherry-pick the equational refactorings as useful in their own right?

[jamesmckinna]

Ugh... that didn't seem to work, sigh, because I hadn't been fine-grained enough about this, or had but reverted too much, yuk.

[jamesmckinna]

Nope. Closing in frustration!