John Major equality is form of

Found at: republic.circumlunar.space:70/~rak/phlog/2021-11-10-John-Major-Equality.md


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

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

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

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