diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 9f7b8af600aa7142310447fdc3d296599d9be3d2..4865f544b02b5de3031547a71cff6dd15324307b 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -51,6 +51,25 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
    format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
 
 (* Texan triples *)
+Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
+  (□ ∀ Φ,
+      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  {{{ x .. y ;  pat ,  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" :=
+  (□ ∀ Φ,
+      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  @  E  {{{ x .. y ;  pat ,  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e {{{ ; pat , Q } } }" :=
+  (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})%I
+    (at level 20,
+     format "{{{  P  } } }  e  {{{ ; pat ,  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" :=
+  (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})%I
+    (at level 20,
+     format "{{{  P  } } }  e  @  E  {{{ ; pat ,  Q } } }") : uPred_scope.
+
 Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
   (∀ Φ : _ → uPred _,
       P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) ⊢ WP e {{ Φ }})