silence fewer warnings, add comment about overwriting notation

@robbertkrebbers could you expand the comment to explain why we are doing this? Seems rather unfortunate.