================================================================
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
