Add reserved notations for `si_pure`.

iris/bi/notation.v

@@ -39,6 +39,9 @@ Reserved Notation "P -∗ Q"
   (at level 99, Q at level 200, right associativity,
    format "'[' P  -∗  '/' '[' Q ']' ']'").
 
+Reserved Notation "<si_pure> Pi" (at level 20, right associativity).
+Reserved Notation "<si_emp_valid> P" (at level 20, right associativity).
+
 Reserved Notation "⎡ P ⎤".
 
 (** Modalities *)