Proposed resolution:

NAD.

[ Post Summit: ]

Alisdair: I was wrong.

Recommend NAD.

[concept.comparison] p2:

Due to the subtle meaning of == inside axioms, the Reflexivity axiom does not do anything as written. It merely states that a value is substitutable with itself, rather than asserting a property of the == operator.

Original proposed resolution:

Change the definition of Reflexivity in [concept.comparison]:

axiom Reflexivity(T a) { (a == a) == true; }