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

stdpp/propset.v

@@ -9,6 +9,13 @@ Global Arguments propset_car {_} _ _ : assert.
 Notation "{[ x | P ]}" := (PropSet (λ x, P))
   (at level 1, format "{[  x  |  P  ]}") : stdpp_scope.
 
+
+Notation "{[ x |@{ A } P ]}" := (PropSet (λ x : A, P))
+  (at level 1, only parsing) : stdpp_scope.
+
+Notation "{[' x | P ]}" := (PropSet (λ x, P))
+  (at level 1, x pattern, format "{['  x  |  P  ]}") : stdpp_scope.
+
 Global Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.
 
 Global Instance propset_top {A} : Top (propset A) := {[ _ | True ]}.