[ refactor ] Add equality as a parameter to Algebra.Consequences.Base

[jamesmckinna]

See this comment on issue #2502 .

By analogy with Algebra.Definitions and Algebra.Structures... moreover non-breaking.
Indeed, Base is only imported by Algebra.Consequences.Setoid (and by the now-deprecated module Algebra.FunctionProperties.Consequences.Core), so there should be no knock-on consequences (sic) for client modules.

[MatthewDaggitt]

Currently this feels like two different PRs merged into one. One with a load of refactorings. One with the change to the equality parameter. Is it possible to separate them out to make them easier to understand and review?

[jamesmckinna]

Currently this feels like two different PRs merged into one. One with a load of refactorings. One with the change to the equality parameter. Is it possible to separate them out to make them easier to understand and review?

Good, thanks @MatthewDaggitt . The 'pure' refactoring PR now split off as #2592 , on which this PR (with the change in top-level parameterisation) then blocks. After merging that (and rebasing this one against the resulting master), this should then be fine to proceed with a lower reviewing burden... I hope ;-)