Fail Notation "x === x" := (eq_refl x) (at level 10).
Reserved Notation "x === x" (only printing, at level 10).
Notation "x === x" := (eq_refl x) (only printing).