move notations into module

[JoJoDeveloping]

This notation is reserved and only used in some parts of the development. But since it is still globally reserved, importing vec.v still produces warnings about clashing notations. A proper fix is to move these notations into a module.

This is a first draft, presumably the definition should also be moved into such a module so that one does not have to re-define the notation elsewhere.

Making the notation no longer globally enabled would be great because it otherwise clashes with the ones defined in FOL/Syntax/SyntacticOps.v.

[DmxLarchey]

@JoJoDeveloping Please have a look at PR #229 that does precisely that among other things. It was only merged in master though.

[JoJoDeveloping]

Oh, thanks for the hint. That seems to do the trick, sad that it's not available on 8.20 yet. So I guess we just wait until you're updated to 9.0.