Added a parallel composition for lambdas over channels

theories/logrel/term_typing_rules.v

@@ -468,6 +468,44 @@ Section properties.
       iExists c1, c2. iSplit=>//. iFrame "Hp1 Hp2".
     Qed.
 
+    Section with_spawn.
+      Context `{spawnG Σ}.
+
+      Definition spar : val :=
+        (λ: "e2" "e1",
+         let: "c" := new_chan #() in
+         ("e1" (Fst "c")) ||| ("e2" (Snd "c")))%V.
+
+      Lemma ltyped_spar Γ Γ1 Γ2 Γ' Γ1' Γ2' e1 e2 S A B :
+        env_split Γ Γ1 Γ2 -∗
+        env_split Γ' Γ1' Γ2' -∗
+        (Γ1 ⊨ e1 : (chan S) ⊸ A ⫤ Γ1') -∗
+        (Γ2 ⊨ e2 : (chan (lty_dual S)) ⊸ B ⫤ Γ2') -∗
+        Γ ⊨ spar e2 e1 : A * B ⫤ Γ'.
+      Proof.
+        iIntros "#Hsplit1 #Hsplit2 #He1 #He2" (vs) "!> HΓ /=".
+        iDestruct ("Hsplit1" with "HΓ") as "[HΓ1 HΓ2]".
+        iDestruct ("He1" with "HΓ1") as "Hv1".
+        iDestruct ("He2" with "HΓ2") as "Hv2".
+        wp_apply (wp_wand with "Hv1").
+        iIntros (v1) "[Hv1 HΓ1']".
+        wp_apply (wp_wand with "Hv2").
+        iIntros (v2) "[Hv2 HΓ2']".
+        wp_lam. wp_pures.
+        wp_apply (new_chan_spec (lsty_car S))=> //.
+        iIntros (c1 c2) "[Hc1 Hc2]".
+        wp_pures.
+        wp_apply (wp_par with "[Hc1 Hv1] [Hc2 Hv2] [HΓ1' HΓ2']").
+        - wp_apply "Hv1". iApply "Hc1".
+        - wp_apply "Hv2". iApply "Hc2".
+        - iIntros (w1 w2) "[Hw1 Hw2]".
+          iSplitL "Hw1 Hw2".
+          + iExists _, _. iFrame. done. 
+          + iApply "Hsplit2". iFrame "HΓ1' HΓ2'".
+      Qed.
+
+    End with_spawn.
+      
     Lemma ltyped_send Γ Γ' (x : string) e A S :
       Γ' !! x = Some (chan (<!!> TY A; S))%lty →
       (Γ ⊨ e : A ⫤ Γ') -∗