diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 75f7ef89b6679d912dd0799ff07479f698a55669..9ec39890f70da033d9fc7d5429d5472423e656ca 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -438,12 +438,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 +460,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.
@@ -471,37 +471,44 @@ Section properties.
     Section with_spawn.
       Context `{spawnG Σ}.
 
-      Definition spar : val :=
-        (λ: "e2" "e1",
+      Definition spar : expr :=
+        (λ: "e1" "e2",
          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 ⫤ Γ'.
+         let: "c1" := Fst "c" in
+         let: "c2" := Snd "c" in
+         ("e1" "c1") ||| ("e2" "c2"))%E.
+
+      Lemma ltyped_spar Γ S A B :
+        ⊢ Γ ⊨ spar : ((chan S) ⊸ A) ⊸ (chan (lty_dual S) ⊸ B) ⊸ 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'".
+        rewrite /spar.
+        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 with_spawn.