Allow pattern and type annotations in propset notation

This allows to use patterns and type annotations in the propset notation, Like {[ (x,y) | ... ]} or {[ x : T | ...]} or even {[ (x, y) : A * B | ...]}.

However, for both the old and new notation, this notation immediately break if someone adds a binary infix | notation downstream, In which case this will be parsed as a singleton of whatever the result of the | operation is. This was already the case before, so anyone that did that already broke the original propset notation