diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index fd770924cef5ccdd6e3ca555968454e126120738..46eeacd91643bd0a442e516dcee464e033290bec 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -7,10 +7,10 @@ Delimit Scope lmsg_scope with lmsg.
 Bind Scope lmsg_scope with lmsg.
 
 Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ :=
-  iMsg_exist M.
+  (∃ v, M v)%msg.
 
 Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
-  iMsg_exist (λ v, iMsg_base v (▷ ltty_car A v) (lsty_car S)).
+  (∃ v, MSG v {{ ▷ ltty_car A v}} ; (lsty_car S))%msg.
 
 Definition lty_end {Σ} : lsty Σ := Lsty END.