For example, instead of: Notation "( X ⊆ )" We now use: Notation "( X ⊆)" We were already doing this for = and ≡. This solves some conflicts with the notations of MetaCoq.