diff --git a/_CoqProject b/_CoqProject
index fc1fc44d4ff96f99e689139723b4097ec117a87c..8fce989b51d1b5d1717fd5f9bc6fcbfa031dda7a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -95,3 +95,4 @@ barrier/specification.v
 barrier/protocol.v
 barrier/proof.v
 barrier/client.v
+examples/joining_existentials.v
diff --git a/examples/joining_extistentials.v b/examples/joining_extistentials.v
new file mode 100644
index 0000000000000000000000000000000000000000..f5fd98f895ec356165e9b96605fe47401742c01e
--- /dev/null
+++ b/examples/joining_extistentials.v
@@ -0,0 +1,7 @@
+From iris.program_logic Require Import saved_one_shot.
+From iris.barrier Require Import proof specification.
+From iris.heap_lang Require Import notation par.
+
+Definition client (eM eW1 eW2 : expr []) : expr [] :=
+  (let: "b" := newbarrier #() in (^^eM ;; ^signal '"b") ||
+                              ((^wait '"b" ;; ^^eW1) || (^wait '"b" ;; ^^eW2))).
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index b8af355587e5e5f24b327cf5283d847f630e0a4d..b72e354dec7ff19a8e078346b60208487e81e2f5 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -228,6 +228,10 @@ Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
   end.
 Solve Obligations with set_solver.
 
+Program Definition wexpr' {X} (e : expr []) : expr X :=
+  wexpr _ e.
+Solve Obligations with set_solver.
+
 Definition of_val' {X} (v : val) : expr X := wexpr (included_nil _) (of_val v).
 
 Lemma wsubst_rec_true_prf {X Y x} (H : X `included` x :: Y) {f y}
@@ -242,7 +246,7 @@ Proof. move: Hfy=>/not_and_l [/dec_stable|/dec_stable]; set_solver. Qed.
 Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
     (H : X `included` x :: Y) (e : expr X)  : expr Y :=
   match e return expr Y with
-  | Var y _ => if decide (x = y) then wexpr _ es else @Var _ y _
+  | Var y _ => if decide (x = y) then wexpr' es else @Var _ y _
   | Rec f y e =>
      Rec f y $ match decide (BNamed x ≠ f ∧ BNamed x ≠ y) return _ with
                | left Hfy => wsubst x es (wsubst_rec_true_prf H Hfy) e
@@ -390,7 +394,7 @@ Lemma wexpr_wsubst X Y Z x es (H1: X `included` x::Y) (H2: Y `included` Z) H3 e:
 Proof.
   revert Y Z H1 H2 H3.
   induction e; intros; repeat (case_decide || simplify_eq/=);
-    auto using var_proof_irrel, wexpr_wexpr with f_equal.
+    unfold wexpr'; auto using var_proof_irrel, wexpr_wexpr with f_equal.
 Qed.
 Lemma wsubst_wexpr X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) H3 e:
   wsubst x es H2 (wexpr H1 e) = wsubst x es H3 e.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 7632623ff4f85fd54516fc59df2b3f38b5560484..9e151bb05dc004cd07980e2928f8d16f643c922f 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -28,6 +28,7 @@ Notation "% l" := (Loc l) (at level 8, format "% l") : expr_scope.
 
 Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
 Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
+Notation "^^ e" := (wexpr' e%E) (at level 8, format "^^ e") : expr_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)