Better notations

[berpeti]

Would it be better to use Coq's (or stdpp's) notations for ML patterns, but with lower index $ml$?

[berpeti]

With the notation changes in Coq 8.20, this might solve our current warnings. Moreover, the precedence levels for all of our notations should be lowered, since they bind weaker than Coq's notations (such as =).