Notation nits and fixed subtyping oversight

theories/logrel/session_types.v

@@ -39,16 +39,17 @@ Notation "∃ x .. y , m" :=
 Notation "'END'" := lty_end : lty_scope.
 Notation "<!!> M" :=
   (lty_message Send M) (at level 200, M at level 200) : lty_scope.
-Notation "<!! x1 .. xn > M" :=
-  (lty_message Send (∃ x1, .. (∃ xn, M) ..))
-    (at level 200, x1 closed binder, xn closed binder, M at level 200,
-     format "<!!  x1  ..  xn >  M") : lty_scope.
+Notation "<!! X .. Y > M" :=
+  (<!!> ∃ X, .. (∃ Y, M) ..)%lty
+    (at level 200, X closed binder, Y closed binder, M at level 200,
+     format "<!!  X  ..  Y >  M") : lty_scope.
+
 Notation "<??> M" :=
   (lty_message Recv M) (at level 200, M at level 200) : lty_scope.
-Notation "<?? x1 .. xn > M" :=
-  (lty_message Recv (∃ x1, .. (∃ xn, M) ..))
-    (at level 200, x1 closed binder, xn closed binder, M at level 200,
-     format "<??  x1  ..  xn >  M") : lty_scope.
+Notation "<?? X .. Y > M" :=
+  (<??> ∃ X, .. (∃ Y, M) ..)%lty
+    (at level 200, X closed binder, Y closed binder, M at level 200,
+     format "<??  X  ..  Y >  M") : lty_scope.
 Notation lty_select := (lty_choice Send).
 Notation lty_branch := (lty_choice Recv).
 Infix "<++>" := lty_app (at level 60) : lty_scope.

theories/logrel/subtyping_rules.v

@@ -260,12 +260,12 @@ Section subtyping_rules.
   Proof. iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto. Qed.
 
   Lemma lty_le_exist_intro_l k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
-    ⊢ (<! X> M X) ⊑ (<!> M A).
-  Proof. by iApply (iProto_le_exist_intro_l). Qed.
+    ⊢ (<!! X> M X) <: (<!!> M A).
+  Proof. iIntros "!>". iApply (iProto_le_exist_intro_l). Qed.
 
   Lemma lty_le_exist_intro_r k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
-    ⊢ (<?> M A) ⊑ (<? X> M X).
-  Proof. by iApply (iProto_le_exist_intro_r). Qed.
+    ⊢ (<??> M A) <: (<?? X> M X).
+  Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
 
   Lemma lty_le_swap_recv_send A1 A2 S :
     ⊢ (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).