Jonas Kastberg · Jonas Kastberg
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
-  Global Instance lty_message_ne a : NonExpansive2 (@lty_message Σ a).
+  Global Instance lty_msg_exist_ne k :
+    Proper (pointwise_relation _ (dist n) ==> (dist n)) (@lty_msg_exist Σ k).
+  Proof. solve_proper. Qed.
+  Global Instance lty_msg_exist_proper k :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (@lty_msg_exist Σ k).
+  Proof. solve_proper. Qed.
+  Global Instance lty_msg_base_ne a : NonExpansive2 (@lty_msg_base Σ a).
+  Proof. rewrite /lty_msg_base. solve_proper. Qed.
+  Global Instance lty_msg_base_proper a :
+    Proper ((≡) ==> (≡) ==> (≡)) (@lty_msg_base Σ a).
+  Proof. rewrite /lty_msg_base. apply ne_proper_2, _. Qed.
+  (* FIXME: Not contractive since lty_msg_exist is not contractive *)
+  (* Global Instance lty_msg_base_contractive n a : *)
+  (*   Proper (dist n ==> dist_later n ==> dist n) (@lty_msg_base Σ a). *)
+  (* Proof. rewrite /lty_msg_base. solve_contractive. Qed. *)
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
    - iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
      by iApply (iProto_le_recv_recv_inv with "H").
  Qed.
+
+  Lemma iProto_le_exist_elim_l_inhabited `{!Inhabited A} (m : A → iMsg Σ V) p :
+    (∀ x, (<?> m x) ⊑ p) -∗
+    (<? x> m x) ⊑ p.
+  Proof.
+    rewrite iMsg_exist_eq. iIntros "H".
+    destruct (iProto_case p) as [Heq | [a [m' Heq]]].
+    - unshelve iSpecialize ("H" $!inhabitant); first by apply _.
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v

    Definition chanrecv : val := λ: "chan", (recv "chan", "chan").
    Lemma ltyped_chanrecv A S :
-      ⊢ ∅ ⊨ chanrecv : chan (<??> A; S) → A * chan S.