diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index daf4eb7f1855bd04c4228b17e1acf1e29af5e477..ef4f749d170b80d7cab3392f4ba4659c1f2b0e0d 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -13,7 +13,7 @@ Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.
 Arguments pvs {_ _ _} _ _ _%I.
 Instance: Params (@pvs) 5.
 
-Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
+Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q)
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }=>  Q") : uPred_scope.
 Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I
@@ -22,7 +22,7 @@ Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I
 Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q)
   (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
 
-Notation "|={ E }=> Q" := (pvs E E Q%I)
+Notation "|={ E }=> Q" := (pvs E E Q)
   (at level 99, E at level 50, Q at level 200,
    format "|={ E }=>  Q") : uPred_scope.
 Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I
@@ -31,7 +31,7 @@ Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I
 Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
   (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
 
-Notation "|={ E1 , E2 }â–·=> Q" := (|={E1%I,E2%I}=> â–· |={E2,E1}=> Q)%I
+Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }â–·=>  Q") : uPred_scope.
 Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 7fdd6ca05604eb642c6b81ddee61d5deb0757a23..d7b188265fdc0767296004247b2ecc4db74eef99 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -4,15 +4,16 @@ From iris.proofmode Require Import pviewshifts invariants.
 Definition vs `{irisG Λ Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P → |={E1,E2}=> Q))%I.
 Arguments vs {_ _ _} _ _ _%I _%I.
+
 Instance: Params (@vs) 5.
-Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
+Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
   (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : uPred_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 ={ E1 , E2 }â–·=> Q" := (P ={E1%I,E2%I}=> â–· |={E2,E1}=> Q)%I
+Notation "P ={ E1 , E2 }â–·=> Q" := (P ={E1,E2}=> â–· |={E2,E1}=> Q)%I
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "P ={ E1 , E2 }â–·=>  Q") : uPred_scope.
 Notation "P ={ E }â–·=> Q" := (P ={E,E}â–·=> Q)%I