diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index b56fa547002c6aaca8f5a9221e81b85952778539..6a2516c926d144b8c4dbbe83687070b7d35b7a9f 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -38,6 +38,8 @@ Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
 Notation "|={ E }=> Q" := (pvs E E Q%I)
   (at level 199, 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.
 
 Section pvs.
 Context {Λ : language} {Σ : iFunctor}.