diff --git a/examples/joining_existentials.v b/examples/joining_existentials.v
index 110e84db265c0e199fdc6987bc6cb19b186c6d03..fdfd528a2a15112138a93979a13421aa9113677e 100644
--- a/examples/joining_existentials.v
+++ b/examples/joining_existentials.v
@@ -28,7 +28,7 @@ Context (P' : iProp) (P P1 P2 Q Q1 Q2 : X → iProp).
 Context {P_split : (∃ x:X, P x) ⊢ ((∃ x:X, P1 x) ★ (∃ x:X, P2 x))}.
 Context {Q_join  : ((∃ x:X, Q1 x) ★ (∃ x:X, Q2 x)) ⊢ (∃ x:X, Q x)}.
 
-Lemma client_spec eM eM' eW1 eW1' eW2 eW2' (R : iProp) :
+Lemma client_spec (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) (R : iProp) :
   eM' = wexpr' eM → eW1' = wexpr' eW1 → eW2' = wexpr' eW2 →
   R ⊢ ({{ P' }} eM {{ λ _, ∃ x, P x }}) →
   R ⊢ (∀ x, {{ P1 x }} eW1 {{ λ _, Q1 x }}) →