Squashed commit of the following:

commit e0d15199
Author: jihgfee <jihgfee@gmail.com>
Date:   Wed Sep 16 14:20:00 2020 +0200

    Refactoring - Moved spar to own file and renamed as par_start

commit fd7dc61d
Author: jihgfee <jihgfee@gmail.com>
Date:   Wed Sep 16 13:10:42 2020 +0200

    Proved spar using typing rule instead of breaking abstraction

commit 821a4c23
Author: jihgfee <jihgfee@gmail.com>
Date:   Tue Sep 15 17:11:20 2020 +0200

    Whitespace cleanup

commit eb01938a
Author: jihgfee <jihgfee@gmail.com>
Date:   Tue Sep 15 17:10:37 2020 +0200

    Added a parallel composition for lambdas over channels

_CoqProject

@@ -36,6 +36,7 @@ theories/logrel/term_typing_judgment.v
 theories/logrel/subtyping_rules.v
 theories/logrel/term_typing_rules.v
 theories/logrel/lib/mutex.v
+theories/logrel/lib/par_start.v
 theories/logrel/examples/double.v
 theories/logrel/examples/pair.v
 theories/logrel/examples/rec_subtyping.v

theories/logrel/lib/par_start.v

+From actris.logrel Require Export term_typing_rules environments.
+From actris.channel Require Import proofmode.
+
+Section properties.
+  Context `{heapG Σ}.
+  Context `{chanG Σ}.
+  Context `{spawnG Σ}.
+
+  Definition par_start : expr :=
+    (λ: "e1" "e2",
+     let: "c" := new_chan #() in
+     let: "c1" := Fst "c" in
+     let: "c2" := Snd "c" in
+     ("e1" "c1") ||| ("e2" "c2"))%E.
+
+  Lemma ltyped_par_start Γ S A B :
+    ⊢ Γ ⊨ par_start : ((chan S) ⊸ A) ⊸ (chan (lty_dual S) ⊸ B) ⊸ A * B.
+  Proof.
+    iApply ltyped_lam; [ iApply env_split_id_l | ].
+    iApply ltyped_lam; [ iApply env_split_id_r | ].
+    iApply ltyped_let.
+    { iApply ltyped_app; [ iApply ltyped_unit | iApply ltyped_new_chan ]. }
+    iApply ltyped_let; [ by iApply ltyped_fst | ].
+    rewrite insert_insert.
+    iApply ltyped_let; [ by iApply ltyped_snd | ].
+    rewrite /binder_insert (insert_commute _ "c1" "c") // insert_insert.
+    iApply (ltyped_par).
+    - iApply env_split_right; last first.
+      { rewrite (insert_commute _ "c1" "e2"); [ | eauto ].
+        rewrite (insert_commute _ "c" "e2"); [ | eauto ].
+        iApply env_split_right; last by iApply env_split_id_r.
+        eauto. eauto. }
+      eauto. eauto.
+    - iApply ltyped_app; by iApply ltyped_var.
+    - iApply ltyped_app; by iApply ltyped_var.
+    - rewrite insert_insert.
+      rewrite (insert_commute _ "c2" "e2") // insert_insert.
+      rewrite (insert_commute _ "c1" "c") // insert_insert.
+      rewrite (insert_commute _ "c1" "e1") //
+              (insert_commute _ "c" "e1") // insert_insert.
+      iApply env_split_left=> //; last first.
+      iApply env_split_left=> //; last first.
+      iApply env_split_left=> //; last first.
+      iApply env_split_id_l.
+      eauto. eauto. eauto.
+  Qed.
+
+End properties.

theories/logrel/term_typing_rules.v

@@ -6,7 +6,8 @@ From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import metatheory.
 From iris.heap_lang.lib Require Export spawn par assert.
-From actris.logrel Require Export subtyping term_typing_judgment operators session_types.
+From actris.logrel Require Export subtyping term_typing_judgment operators
+     session_types.
 From actris.logrel Require Import environments.
 From actris.utils Require Import switch.
 From actris.channel Require Import proofmode.
@@ -438,12 +439,12 @@ Section properties.
     (** Parallel composition properties *)
     Lemma ltyped_par Γ Γ' Γ1 Γ1' Γ2 Γ2' e1 e2 A B :
       env_split Γ Γ1 Γ2 -∗
-      env_split Γ' Γ1' Γ2' -∗
       (Γ1 ⊨ e1 : A ⫤ Γ1') -∗
       (Γ2 ⊨ e2 : B ⫤ Γ2') -∗
+      env_split Γ' Γ1' Γ2' -∗
       Γ ⊨ e1 ||| e2 : A * B ⫤ Γ'.
     Proof.
-      iIntros "#Hsplit #Hsplit' #H1 #H2" (vs) "!> HΓ /=".
+      iIntros "#Hsplit #H1 #H2 #Hsplit'" (vs) "!> HΓ /=".
       iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
       wp_apply (wp_par with "[HΓ1] [HΓ2]").
       - iApply ("H1" with "HΓ1").
@@ -460,10 +461,10 @@ Section properties.
     Context `{chanG Σ}.
 
     Lemma ltyped_new_chan Γ S :
-      ⊢ Γ ⊨ new_chan : () → (chan S * chan (lty_dual S)) ⫤ Γ.
+      ⊢ Γ ⊨ new_chan : () ⊸ (chan S * chan (lty_dual S)) ⫤ Γ.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value. iFrame "HΓ".
-      iIntros "!>" (u) ">->".
+      iIntros (u) ">->".
       iApply (new_chan_spec with "[//]"); iIntros (c1 c2) "!> [Hp1 Hp2]".
       iExists c1, c2. iSplit=>//. iFrame "Hp1 Hp2".
     Qed.