diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 27abe6a5269ba9e8cfa2ed3533233baac48202e9..9bddbbb8b7cec241a216317ee3abdc29f7b59201 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -30,3 +30,14 @@
      let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{ _, True }}
   
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  fun1, fun2, fun3 : expr
+  ============================
+  {{{ True }}}
+    let: "val1" := fun1 #() in
+    let: "val2" := fun2 "val1" in
+    let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
+  {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index bcc2e47de76d4dda4bc91f7f2a6486b82dd67364..962c4a5ca6e440dbe96b4fb31544d3b007617e4a 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -128,6 +128,15 @@ Section printing_tests.
     iIntros "_". Show.
   Abort.
 
+  Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
+    {{{ True }}}
+       let: "val1" := fun1 #() in
+       let: "val2" := fun2 "val1" in
+       let: "val3" := fun3 "val2" in
+       if: "val1" = "val2" then "val" else "val3"
+    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
+  Proof. Show. Abort.
+
 End printing_tests.
 
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index bf585cc9c3e98c63024c4b3130ccab54ba8b5d7c..6382b8046517ea0d2742eaff147d2a0fac577f99 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -89,93 +89,75 @@ Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  s ;  E  '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' 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 ,  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  E  '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' 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 ,  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  E  ? '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e {{{ x .. y , 'RET' 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 ,   RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' 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 ,   RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  ? '/' {{{  x  ..  y ,   RET  pat ;  Q  } } } ']'") : bi_scope.
+
 Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  s ;  E  '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  E  '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  E  ? '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  {{{  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  ? '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
 
+(* Aliases for stdpp scope -- they inherit the levels and format from above. *)
 Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})
-    (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})
-    (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})
-    (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})
-    (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})
-    (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})
-    (at level 20,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})
-    (at level 20,
-     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})
-    (at level 20,
-     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q  } } }") : stdpp_scope.
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})
-    (at level 20,
-     format "{{{  P  } } }  e  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})
-    (at level 20,
-     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q  } } }") : stdpp_scope.
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }}) : stdpp_scope.
 
 Section wp.
 Context `{irisG Λ Σ}.