propagate change to equality semantics upwards

this might break the translator (untested).
compiler proofs build, though.