diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 51c23f4769d970ed9bbe064baf413456aa754799..cd2ee4887ec56bcc3bfa49a88b5286945ef374c1 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -33,13 +33,13 @@ Arguments pvs {_ _} _ _ _%I.
 Instance: Params (@pvs) 4.
 
 Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
-  (at level 199, E1, E2 at level 50, Q at level 200,
+  (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }=>  Q") : uPred_scope.
 Notation "|={ E }=> Q" := (pvs E E Q%I)
-  (at level 199, E at level 50, Q at level 200,
+  (at level 99, E at level 50, Q at level 200,
    format "|={ E }=>  Q") : uPred_scope.
 Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
-  (at level 199, Q at level 200, format "|==>  Q") : uPred_scope.
+  (at level 99, Q at level 200, format "|==>  Q") : uPred_scope.
 
 Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index eb1c9154394b614dd9723081110ec01e79ddfcb0..5bf652bac7b7c199e149c0ec6330ebceff6fd5ac 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -8,15 +8,30 @@ Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
 Arguments vs {_ _} _ _ _%I _%I.
 Instance: Params (@vs) 4.
 Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
-  (at level 199, E1,E2 at level 50,
+  (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : uPred_scope.
-Notation "P ={ E1 , E2 }=> Q" := (True ⊢ vs E1 E2 P%I Q%I)
-  (at level 199, E1, E2 at level 50,
+Notation "P ={ E1 , E2 }=> Q" := (True ⊢ (P ={E1,E2}=> Q)%I)
+  (at level 99, E1, E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : C_scope.
-Notation "P ={ E }=> Q" := (vs E E P%I Q%I)
-  (at level 199, E at level 50, format "P  ={ E }=>  Q") : uPred_scope.
-Notation "P ={ E }=> Q" := (True ⊢ vs E E P%I Q%I)
-  (at level 199, E at level 50, format "P  ={ E }=>  Q") : C_scope.
+Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=>  Q") : uPred_scope.
+Notation "P ={ E }=> Q" := (True ⊢ (P ={E}=> Q)%I)
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=>  Q") : C_scope.
+
+Notation "P <={ E1 , E2 }=> Q" := ((P ={E1,E2}=> Q) ∧ (Q ={E2,E1}=> P))%I
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  <={ E1 , E2 }=>  Q") : uPred_scope.
+Notation "P <={ E1 , E2 }=> Q" := (True ⊢ (P <={E1,E2}=> Q)%I)
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "P  <={ E1 , E2 }=>  Q") : C_scope.
+Notation "P <={ E }=> Q" := (P <={E,E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  <={ E }=>  Q") : uPred_scope.
+Notation "P <={ E }=> Q" := (True ⊢ (P <={E}=> Q)%I)
+  (at level 99, E at level 50, Q at level 200,
+   format "P  <={ E }=>  Q") : C_scope.
 
 Section vs.
 Context {Λ : language} {Σ : iFunctor}.