middle four exchange law in a Setoid: definition and consequences

[jamesmckinna]

_MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
_*_ MiddleFourExchange _+_ =  ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z))

UPDATED: hmmm... naming conventions between Algebra.Consequences.Setoid and Algebra.Consequences.Propositional: may wish to remove cong+ prefixes? DONE.

[gallais]

There's a lot of misaligned type signature, probably due to the fact that
some lemmas were renamed during the preparation of this PR.

Other than that, it looks OK to me.

[jamesmckinna]

This must be a common problem, but the alignment still looks off in the GitHub listing, while looks fine in my vanilla default Emacs (GNU Emacs 26.3) font under Linux (Ubuntu 20.04LTS). What is the (FAQ?) recommendation of suitable fixed-width fonts to use in Emacs?

[gallais]

Yes the whitespace alignment in your types seems to be off by one.
In emacs using DejaVu Sans Mono I also see the off by one issue.