2021-11-10: John Major Equality                              rak
================================================================

John Major equality [0,1] is a form of heterogenous equality
used to simplify statements of equality facts. Adam Chlipala
writes that:

> The identifier JMeq stands for "John Major equality," a name
> coined by Conor McBride as an inside joke about British
> politics. [1]

In McBride's original paper [2], the "inside joke" is:

> I call this 'John Major' equality, because it widens
> aspirations to equality without affecting the practical
> outcome.

I know John Major was prime minister in the 1990s. To what,
exactly, is this joke referring to?

[0]: https://coq.inria.fr/library/Coq.Logic.JMeq.html
[1]: http://adam.chlipala.net/cpdt/html/Equality.html
[2]: http://www.e-pig.org/downloads/elim.pdf