diff --git a/_CoqProject b/_CoqProject
index 31a0aac47e4963d518f1e68a38d8dd61c5d44d70..43f1f574e191bce8bdc0a8612450ff8f8358e5d6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -27,5 +27,6 @@ theories/logrel/operators.v
 theories/logrel/term_typing_judgment.v
 theories/logrel/subtyping_rules.v
 theories/logrel/term_typing_rules.v
+theories/logrel/lib/mutex.v
 theories/logrel/examples/double.v
 theories/logrel/examples/pair.v
diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
new file mode 100644
index 0000000000000000000000000000000000000000..95a8249089c7a6f0f9bbb2d379ac7a169220c0e7
--- /dev/null
+++ b/theories/logrel/lib/mutex.v
@@ -0,0 +1,145 @@
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Export spin_lock.
+From actris.logrel Require Export term_types term_typing_judgment subtyping.
+From actris.logrel Require Import environments.
+From actris.channel Require Import proofmode.
+From iris.heap_lang Require Import metatheory.
+
+(** Mutex functions *)
+Definition mutex_alloc : val := λ: "x", (newlock #(), ref "x").
+Definition mutex_acquire : val := λ: "x", acquire (Fst "x");; ! (Snd "x").
+Definition mutex_release : val :=
+  λ: "guard" "inner", Snd "guard" <- "inner";; release (Fst "guard").
+
+(** Semantic types *)
+Definition lty_mutex `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
+  ∃ (γ : gname) (l : loc) (lk : val),
+    ⌜ w = PairV lk #l ⌝ ∗
+    is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner))%I.
+
+Definition lty_mutex_guard `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
+  ∃ (γ : gname) (l : loc) (lk : val) (v : val),
+    ⌜ w = PairV lk #l ⌝ ∗
+    is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner) ∗
+    spin_lock.locked γ ∗ l ↦ v)%I.
+
+Instance: Params (@lty_mutex) 3 := {}.
+Instance: Params (@lty_mutex_guard) 3 := {}.
+
+Notation "'mutex' A" := (lty_mutex A) (at level 10) : lty_scope.
+Notation "'mutex_guard' A" := (lty_mutex_guard A) (at level 10) : lty_scope.
+
+Section properties.
+  Context `{heapG Σ, lockG Σ}.
+  Implicit Types A : ltty Σ.
+
+  Global Instance lty_mutex_contractive : Contractive lty_mutex.
+  Proof. solve_contractive. Qed.
+  Global Instance lty_mutex_ne : NonExpansive lty_mutex.
+  Proof. solve_proper. Qed.
+
+  Global Instance lty_mutex_guard_contractive :
+    Contractive lty_mutex_guard.
+  Proof. solve_contractive. Qed.
+  Global Instance lty_mutex_guard_ne : NonExpansive lty_mutex_guard.
+  Proof. solve_proper. Qed.
+
+  Lemma lty_le_mutex A1 A2 :
+    ▷ (A1 <:> A2) -∗
+    mutex A1 <: mutex A2.
+  Proof.
+    iIntros "#[Hle1 Hle2]" (v) "!>". iDestruct 1 as (γ l lk ->) "Hinv".
+    iExists γ, l, lk. iSplit; first done.
+    iApply (spin_lock.is_lock_iff with "Hinv").
+    iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
+  Qed.
+
+  Lemma lty_copyable_mutex A :
+    ⊢ lty_copyable (mutex A).
+  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+  Lemma lty_le_mutex_guard A1 A2 :
+    ▷ (A1 <:> A2) -∗
+    mutex_guard A1 <: mutex_guard A2.
+  Proof.
+    iIntros "#[Hle1 Hle2]" (v) "!>".
+    iDestruct 1 as (γ l lk w ->) "[Hinv [Hlock Hinner]]".
+    iExists γ, l, lk, w. iSplit; first done.
+    iFrame "Hlock Hinner". iApply (spin_lock.is_lock_iff with "Hinv").
+    iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
+  Qed.
+End properties.
+
+Section rules.
+  Context `{heapG Σ, lockG Σ}.
+
+  (** Mutex properties *)
+  Lemma ltyped_mutex_alloc A :
+    ⊢ ∅ ⊨ mutex_alloc : A → mutex A.
+  Proof.
+    iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
+    iIntros "!>" (v) "Hv". rewrite /mutex_alloc. wp_pures.
+    wp_alloc l as "Hl".
+    wp_bind (newlock _).
+    set (N := nroot .@ "makelock").
+    iAssert (∃ inner, l ↦ inner ∗ ltty_car A inner)%I with "[Hl Hv]" as "Hlock".
+    { iExists v. iFrame "Hl Hv". }
+    wp_apply (newlock_spec with "Hlock").
+    iIntros (lk γ) "Hlock".
+    wp_pures. iExists γ, l, lk. iSplit=> //.
+  Qed.
+
+  Lemma ltyped_mutex_acquire Γ (x : string) A :
+    Γ !! x = Some (mutex A)%lty →
+    ⊢ Γ ⊨ mutex_acquire x : A ⫤ <[x := (mutex_guard A)%lty]> Γ.
+  Proof.
+    iIntros (Hx vs) "!> HΓ /=".
+    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv.
+    rewrite /mutex_acquire. wp_pures.
+    iDestruct "HA" as (γ l lk ->) "#Hlock".
+    wp_bind (acquire _).
+    wp_apply (acquire_spec with "Hlock"). iIntros "[Hlocked Hinner]".
+    iDestruct "Hinner" as (v) "[Hl HA]".
+    wp_pures. wp_load.
+    iFrame "HA".
+    iAssert (ltty_car (mutex_guard A)%lty (lk, #l)) with "[Hlocked Hl]" as "Hguard".
+    { iExists γ, l, lk, v. iSplit=>//. iFrame "Hlocked Hl Hlock". }
+    iDestruct (env_ltyped_insert _ _ x with "Hguard HΓ") as "HΓ".
+    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
+    iFrame "HΓ".
+  Qed.
+
+  Lemma ltyped_mutex_release Γ Γ' (x : string) e A :
+    Γ' !! x = Some (mutex_guard A)%lty →
+    (Γ ⊨ e : A ⫤ Γ') -∗
+    Γ ⊨ mutex_release x e : () ⫤ <[x := (mutex A)%lty]> Γ'.
+  Proof.
+    iIntros (Hx) "#He". iIntros (vs) "!> HΓ /=".
+    wp_bind (subst_map vs e).
+    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[HA HΓ']".
+    iDestruct (env_ltyped_lookup with "HΓ'") as (g Hg) "[Hguard HΓ']"; first done; rewrite Hg.
+    iDestruct "Hguard" as (γ l lk inner ->) "(#Hlock & Hlocked & Hinner)".
+    rewrite /mutex_release.
+    wp_pures. wp_store. wp_pures.
+    iAssert (∃ inner, l ↦ inner ∗ ltty_car A inner)%I
+      with "[Hinner HA]" as "Hinner".
+    { iExists v. iFrame "Hinner HA". }
+    wp_apply (release_spec γ _ (∃ inner, l ↦ inner ∗ ltty_car A inner)%I
+                with "[Hlocked Hinner]").
+    { iFrame "Hlock Hlocked".
+      iDestruct "Hinner" as (w) "[Hl HA]". eauto with iFrame. }
+    iIntros "_". wp_pures.
+    iSplit=> //.
+    iAssert (ltty_car (mutex A)%lty (lk, #l)) with "[Hlock]" as "Hmutex".
+    { iExists γ, l, lk. iSplit=>//. }
+    iDestruct (env_ltyped_insert _ _ x with "Hmutex HΓ'") as "HΓ'".
+    rewrite /binder_insert insert_delete (insert_id _ _ _ Hg).
+    iFrame "HΓ'".
+  Qed.
+
+End rules.
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 0c1b29206d0dd072cc7335d1024bbf2f21bcfa57..6a3aa6f4ffee5ddb5d9983443214890260ae43b5 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -171,7 +171,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_exist C1 C2 :
-    ▷ (∀ A, C1 A <: C2 A) -∗
+    (∀ A, C1 A <: C2 A) -∗
     (∃ A, C1 A) <: (∃ A, C2 A).
   Proof.
     iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle".
@@ -187,7 +187,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_copyable_exist (C : ltty Σ → ltty Σ) :
-    ▷ (∀ M, lty_copyable (C M)) -∗ lty_copyable (lty_exist C).
+    (∀ M, lty_copyable (C M)) -∗ lty_copyable (lty_exist C).
   Proof.
     iIntros "#Hle". rewrite /lty_copyable /tc_opaque.
     iApply lty_le_r; last by iApply lty_le_exist_copy.
@@ -236,33 +236,6 @@ Section subtyping_rules.
     ⊢ lty_copyable (ref_shr A).
   Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
 
-  Lemma lty_le_mutex A1 A2 :
-    ▷ (A1 <:> A2) -∗
-    mutex A1 <: mutex A2.
-  Proof.
-    iIntros "#[Hle1 Hle2]" (v) "!>". iDestruct 1 as (γ l lk ->) "Hinv".
-    iExists γ, l, lk. iSplit; first done.
-    iApply (spin_lock.is_lock_iff with "Hinv").
-    iIntros "!> !>". iSplit.
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
-  Qed.
-  Lemma lty_copyable_mutex A :
-    ⊢ lty_copyable (mutex A).
-  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
-
-  Lemma lty_le_mutexguard A1 A2 :
-    ▷ (A1 <:> A2) -∗
-    mutexguard A1 <: mutexguard A2.
-  Proof.
-    iIntros "#[Hle1 Hle2]" (v) "!>".
-    iDestruct 1 as (γ l lk w ->) "[Hinv [Hlock Hinner]]".
-    iExists γ, l, lk, w. iSplit; first done.
-    iFrame "Hlock Hinner". iApply (spin_lock.is_lock_iff with "Hinv").
-    iIntros "!> !>". iSplit.
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
-  Qed.
 
   Lemma lty_le_chan S1 S2 :
     ▷ (S1 <: S2) -∗ chan S1 <: chan S2.
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index 329318faca9a5d4d04225e8e2b4830517013343b..82d6e3c3ec327b3dd79fb1f87a22f672710af6a0 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -7,7 +7,7 @@ From actris.channel Require Export channel.
 Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
 
 Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, □ ltty_car A w)%I.
-Definition lty_copy_inv {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
+Definition lty_copy_minus {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
 Definition lty_copyable {Σ} (A : ltty Σ) : iProp Σ :=
   tc_opaque (A <: lty_copy A)%I.
 
@@ -27,7 +27,7 @@ Definition lty_sum {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
 Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∀ A, WP w #() {{ ltty_car (C A) }})%I.
 Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
-  Ltty (λ w, ∃ A, ▷ ltty_car (C A) w)%I.
+  Ltty (λ w, ∃ A, ltty_car (C A) w)%I.
 
 Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ ltty_car A v)%I.
@@ -35,21 +35,11 @@ Definition ref_shrN := nroot .@ "shr_ref".
 Definition lty_ref_shr `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ l : loc, ⌜w = #l⌝ ∗ inv (ref_shrN .@ l) (∃ v, l ↦ v ∗ ltty_car A v))%I.
 
-Definition lty_mutex `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
-  ∃ (γ : gname) (l : loc) (lk : val),
-    ⌜ w = PairV lk #l ⌝ ∗
-    is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner))%I.
-Definition lty_mutexguard `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
-  ∃ (γ : gname) (l : loc) (lk : val) (v : val),
-    ⌜ w = PairV lk #l ⌝ ∗
-    is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner) ∗
-    spin_lock.locked γ ∗ l ↦ v)%I.
-
 Definition lty_chan `{heapG Σ, chanG Σ} (P : lsty Σ) : ltty Σ :=
   Ltty (λ w, w ↣ lsty_car P)%I.
 
 Instance: Params (@lty_copy) 1 := {}.
-Instance: Params (@lty_copy_inv) 1 := {}.
+Instance: Params (@lty_copy_minus) 1 := {}.
 Instance: Params (@lty_copyable) 1 := {}.
 Instance: Params (@lty_arr) 2 := {}.
 Instance: Params (@lty_prod) 1 := {}.
@@ -58,14 +48,12 @@ Instance: Params (@lty_forall) 2 := {}.
 Instance: Params (@lty_sum) 1 := {}.
 Instance: Params (@lty_ref_mut) 2 := {}.
 Instance: Params (@lty_ref_shr) 2 := {}.
-Instance: Params (@lty_mutex) 3 := {}.
-Instance: Params (@lty_mutexguard) 3 := {}.
 Instance: Params (@lty_chan) 3 := {}.
 
 Notation any := lty_any.
 Notation "()" := lty_unit : lty_scope.
 Notation "'copy' A" := (lty_copy A) (at level 10) : lty_scope.
-Notation "'copy-' A" := (lty_copy_inv A) (at level 10) : lty_scope.
+Notation "'copy-' A" := (lty_copy_minus A) (at level 10) : lty_scope.
 
 Notation "A ⊸ B" := (lty_arr A B)
   (at level 99, B at level 200, right associativity) : lty_scope.
@@ -81,9 +69,6 @@ Notation "∃ A1 .. An , C" :=
 Notation "'ref_mut' A" := (lty_ref_mut A) (at level 10) : lty_scope.
 Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : lty_scope.
 
-Notation "'mutex' A" := (lty_mutex A) (at level 10) : lty_scope.
-Notation "'mutexguard' A" := (lty_mutexguard A) (at level 10) : lty_scope.
-
 Notation "'chan' A" := (lty_chan A) (at level 10) : lty_scope.
 
 Section term_types.
@@ -92,7 +77,7 @@ Section term_types.
 
   Global Instance lty_copy_ne : NonExpansive (@lty_copy Σ).
   Proof. solve_proper. Qed.
-  Global Instance lty_copy_inv_ne : NonExpansive (@lty_copy_inv Σ).
+  Global Instance lty_copy_minus_ne : NonExpansive (@lty_copy_minus Σ).
   Proof. solve_proper. Qed.
 
   Global Instance lty_copyable_plain A : Plain (lty_copyable A).
@@ -130,9 +115,6 @@ Section term_types.
   Global Instance lty_forall_ne `{heapG Σ} k n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).
   Proof. solve_proper. Qed.
-  Global Instance lty_exist_contractive k n :
-    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ k).
-  Proof. solve_contractive. Qed.
   Global Instance lty_exist_ne k n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k).
   Proof. solve_proper. Qed.
@@ -147,17 +129,6 @@ Section term_types.
   Global Instance lty_ref_shr_ne `{heapG Σ} : NonExpansive lty_ref_shr.
   Proof. solve_proper. Qed.
 
-  Global Instance lty_mutex_contractive `{heapG Σ, lockG Σ} : Contractive lty_mutex.
-  Proof. solve_contractive. Qed.
-  Global Instance lty_mutex_ne `{heapG Σ, lockG Σ} : NonExpansive lty_mutex.
-  Proof. solve_proper. Qed.
-
-  Global Instance lty_mutexguard_contractive `{heapG Σ, lockG Σ} :
-    Contractive lty_mutexguard.
-  Proof. solve_contractive. Qed.
-  Global Instance lty_mutexguard_ne `{heapG Σ, lockG Σ} : NonExpansive lty_mutexguard.
-  Proof. solve_proper. Qed.
-
   Global Instance lty_chan_ne `{heapG Σ, chanG Σ} : NonExpansive lty_chan.
   Proof. solve_proper. Qed.
 End term_types.
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 934a9ff29d468d4e9652747847744e23b1885c26..17c7797e4d8cdd7805c4b8a4fd3d1781aab61a73 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -14,19 +14,6 @@ Notation "Γ ⊨ e : A ⫤ Γ'" := (ltyped Γ Γ' e A)
 Notation "Γ ⊨ e : A" := (Γ ⊨ e : A ⫤ Γ)
   (at level 100, e at next level, A at level 200).
 
-Lemma ltyped_frame `{!heapG Σ} (Γ Γ' Γ1 Γ1' Γ2 : gmap string (ltty Σ)) e A :
-  env_split Γ Γ1 Γ2 -∗
-  env_split Γ' Γ1' Γ2 -∗
-  (Γ1 ⊨ e : A ⫤ Γ1') -∗
-  Γ ⊨ e : A ⫤ Γ'.
-Proof.
-  iIntros "#Hsplit #Hsplit' #Htyped !>" (vs) "Henv".
-  iDestruct ("Hsplit" with "Henv") as "[Henv1 Henv2]".
-  iApply (wp_wand with "(Htyped Henv1)").
-  iIntros (v) "[$ Henv1']".
-  iApply "Hsplit'". iFrame "Henv1' Henv2".
-Qed.
-
 Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
   (∀ `{heapG Σ}, ∃ A Γ', ⊢ ∅ ⊨ e : A ⫤ Γ') →
   rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 54e5fddab5839935298bf522ae79ea18388d5ddb..b5d3585e74862dbe3caac54ee1f68a66f8c59262 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -14,16 +14,32 @@ Section properties.
   Implicit Types S T : lsty Σ.
   Implicit Types Γ : gmap string (ltty Σ).
 
+  (** Frame rule *)
+  Lemma ltyped_frame Γ Γ' Γ1 Γ1' Γ2 e A :
+    env_split Γ Γ1 Γ2 -∗
+    env_split Γ' Γ1' Γ2 -∗
+    (Γ1 ⊨ e : A ⫤ Γ1') -∗
+    Γ ⊨ e : A ⫤ Γ'.
+  Proof.
+    iIntros "#Hsplit #Hsplit' #Htyped !>" (vs) "Henv".
+    iDestruct ("Hsplit" with "Henv") as "[Henv1 Henv2]".
+    iApply (wp_wand with "(Htyped Henv1)").
+    iIntros (v) "[$ Henv1']".
+    iApply "Hsplit'". iFrame "Henv1' Henv2".
+  Qed.
+
   (** Variable properties *)
   Lemma ltyped_var Γ (x : string) A :
-    Γ !! x = Some A → ⊢ Γ ⊨ x : A ⫤ <[x:=copy- A]>%lty Γ.
+    Γ !! x = Some A → ⊢ Γ ⊨ x : A ⫤ <[x := (copy- A)%lty]> Γ.
   Proof.
     iIntros (HΓx) "!>"; iIntros (vs) "HΓ /=".
-    iDestruct (env_ltyped_lookup with "HΓ") as (v Hx) "[HA HΓ]"; first done.
-    rewrite Hx. iApply wp_value.
-    iDestruct (coreP_intro with "HA") as "#HAc". iFrame "HA".
-    iEval (rewrite -insert_delete -(insert_id vs x v) //).
-    by iApply (env_ltyped_insert _ _ x).
+    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv.
+    iApply wp_value.
+    iAssert (ltty_car (copy- A) v)%lty as "#HAm". { iApply coreP_intro. iApply "HA". }
+    iFrame "HA".
+    iDestruct (env_ltyped_insert _ _ x with "HAm HΓ") as "HΓ".
+    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
+    iApply "HΓ".
   Qed.
 
   (** Subtyping *)
@@ -71,9 +87,9 @@ Section properties.
   Qed.
 
   (* Typing rule for introducing copyable functions *)
-  Lemma ltyped_rec Γ Γ' f x e A1 A2 :
+  Lemma ltyped_rec Γ Γ' Γ'' f x e A1 A2 :
     env_copy Γ Γ' -∗
-    (binder_insert f (A1 → A2)%lty (binder_insert x A1 Γ') ⊨ e : A2) -∗
+    (binder_insert f (A1 → A2)%lty (binder_insert x A1 Γ') ⊨ e : A2 ⫤ Γ'') -∗
     Γ ⊨ (rec: f x := e) : A1 → A2 ⫤ ∅.
   Proof.
     iIntros "#Hcopy #He". iIntros (vs) "!> HΓ /=". iApply wp_fupd. wp_pures.
@@ -112,45 +128,6 @@ Section properties.
     iApply env_ltyped_delete=> //.
   Qed.
 
-  Fixpoint lty_arr_list (As : list (ltty Σ)) (B : ltty Σ) : ltty Σ :=
-    match As with
-    | [] => B
-    | A :: As => A ⊸ lty_arr_list As B
-    end.
-
-  Lemma lty_arr_list_spec_step A As (e : expr) B ws y i :
-    (∀ v, ltty_car A v -∗
-      WP subst_map (<[y+:+pretty i:=v]> ws)
-         (switch_lams y (S i) (length As) e) {{ ltty_car (lty_arr_list As B) }}) -∗
-    WP subst_map ws (switch_lams y i (S (length As)) e)
-       {{ ltty_car (lty_arr_list (A :: As) B) }}.
-  Proof.
-    iIntros "H". wp_pures. iIntros (v) "HA".
-    iDestruct ("H" with "HA") as "H".
-    rewrite subst_map_insert.
-    wp_apply "H".
-  Qed.
-
-  Lemma lty_arr_list_spec As (e : expr) B ws y i n :
-    n = length As →
-    (∀ vs, ([∗ list] A;v ∈ As;vs, ltty_car A v) -∗
-           WP subst_map (map_string_seq y i vs ∪ ws) e {{ ltty_car B }}) -∗
-    WP subst_map ws (switch_lams y i n e) {{ ltty_car (lty_arr_list As B) }}.
-  Proof.
-    iIntros (Hlen) "H".
-    iInduction As as [|A As] "IH" forall (ws i e n Hlen); simplify_eq/=.
-    - iDestruct ("H" $! [] with "[$]") as "H"=> /=.
-      by rewrite left_id_L.
-    - iApply lty_arr_list_spec_step. iIntros (v) "HA".
-      iApply ("IH" with "[//]"). iIntros (vs) "HAs".
-      iSpecialize ("H" $! (v::vs)); simpl.
-      do 2 rewrite insert_union_singleton_l.
-      rewrite (map_union_comm ({[y +:+ pretty i := v]})); last first.
-      { apply map_disjoint_singleton_l_2.
-        apply lookup_map_string_seq_None_lt. eauto. }
-      rewrite assoc_L. iApply ("H" with "[$HA $HAs]").
-  Qed.
-
   (** Product properties  *)
   Lemma ltyped_pair Γ1 Γ2 Γ3 e1 e2 A1 A2 :
     (Γ2 ⊨ e1 : A1 ⫤ Γ3) -∗ (Γ1 ⊨ e2 : A2 ⫤ Γ2) -∗
@@ -162,19 +139,38 @@ Section properties.
     wp_pures. iFrame "HΓ". iExists w1, w2. by iFrame.
   Qed.
 
-  Definition split : val := λ: "pair" "f", "f" (Fst "pair") (Snd "pair").
+  Lemma ltyped_fst Γ A1 A2 (x : string) :
+    Γ !! x = Some (A1 * A2)%lty →
+    ⊢ Γ ⊨ Fst x : A1 ⫤ <[x := (copy- A1 * A2)%lty]> Γ.
+  Proof.
+    iIntros (Hx vs) "!> HΓ /=".
+    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv.
+    iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]".
+    wp_pures.
+    iAssert (ltty_car (copy- A1) v1)%lty as "#HA1m". { iApply coreP_intro. iApply "HA1". }
+    iFrame "HA1".
+    iAssert (ltty_car (copy- A1 * A2) (v1, v2))%lty with "[HA2]" as "HA".
+    { iExists v1, v2. iSplit=>//. iFrame "HA1m HA2". }
+    iDestruct (env_ltyped_insert _ _ x with "HA HΓ") as "HΓ".
+    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
+    iFrame "HΓ".
+  Qed.
 
-  Lemma ltyped_split A1 A2 B :
-    ⊢ ∅ ⊨ split : A1 * A2 → (A1 ⊸ A2 ⊸ B) ⊸ B.
+  Lemma ltyped_snd Γ A1 A2 (x : string) :
+    Γ !! x = Some (A1 * A2)%lty →
+    ⊢ Γ ⊨ Snd x : A2 ⫤ <[x := (A1 * copy- A2)%lty]> Γ.
   Proof.
-    iIntros (vs) "!> HΓ /=". iApply wp_value.
-    iSplitL; last by iApply env_ltyped_empty.
-    iIntros "!>" (v) "Hv". rewrite /split. wp_pures.
-    iDestruct "Hv" as (w1 w2 ->) "[Hw1 Hw2]".
-    iIntros (f) "Hf". wp_pures.
-    iPoseProof ("Hf" with "Hw1") as "Hf".
-    wp_apply (wp_wand with "Hf").
-    iIntros (g) "Hg". iApply ("Hg" with "Hw2").
+    iIntros (Hx vs) "!> HΓ /=".
+    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv.
+    iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]".
+    wp_pures.
+    iAssert (ltty_car (copy- A2) v2)%lty as "#HA2m". { iApply coreP_intro. iApply "HA2". }
+    iFrame "HA2".
+    iAssert (ltty_car (A1 * copy- A2) (v1, v2))%lty with "[HA1]" as "HA".
+    { iExists v1, v2. iSplit=>//. iFrame "HA2m HA1". }
+    iDestruct (env_ltyped_insert _ _ x with "HA HΓ") as "HΓ".
+    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
+    iFrame "HΓ".
   Qed.
 
   (** Sum Properties *)
@@ -196,24 +192,27 @@ Section properties.
     iRight. iExists v. auto.
   Qed.
 
-  Definition paircase : val := λ: "pair" "left" "right",
-    Case "pair" "left" "right".
-
-  Lemma ltyped_paircase A1 A2 B :
-    ⊢ ∅ ⊨ paircase : A1 + A2 → (A1 ⊸ B) ⊸ (A2 ⊸ B) ⊸ B.
+  (* TODO: This probably requires there to be a rule that allows dropping arbitrary
+  resources from the postcondition. Check if there is such a rule. *)
+  Lemma ltyped_case Γ1 Γ2 Γ3 e1 e2 e3 A1 A2 B :
+    (Γ1 ⊨ e1 : A1 + A2 ⫤ Γ2) -∗
+    (Γ2 ⊨ e2 : A1 ⊸ B ⫤ Γ3) -∗
+    (Γ2 ⊨ e3 : A2 ⊸ B ⫤ Γ3) -∗
+    (Γ1 ⊨ Case e1 e2 e3 : B ⫤ Γ3).
   Proof.
-    iIntros (vs) "!> HΓ /=". iApply wp_value.
-    iSplitL; last by iApply env_ltyped_empty.
-    rewrite /paircase. iIntros "!>" (p) "Hp". wp_pures.
-    iIntros (f_left) "Hleft". wp_pures.
-    iIntros (f_right) "Hright". wp_pures.
-    iDestruct "Hp" as "[Hp|Hp]".
-    - iDestruct "Hp" as (w1 ->) "Hp". wp_pures.
-      wp_apply (wp_wand with "(Hleft [Hp //])").
-      iIntros (v) "HB". iApply "HB".
-    - iDestruct "Hp" as (w2 ->) "Hp". wp_pures.
-      wp_apply (wp_wand with "(Hright [Hp //])").
-      iIntros (v) "HB". iApply "HB".
+    iIntros "#H1 #H2 #H3" (vs) "!> HΓ1 /=".
+    wp_bind (subst_map vs e1).
+    iSpecialize ("H1" with "HΓ1").
+    iApply (wp_wand with "H1"). iIntros (s) "[Hs HΓ2]".
+    iDestruct "Hs" as "[Hs|Hs]"; iDestruct "Hs" as (w ->) "HA"; wp_case.
+    - wp_bind (subst_map vs e2).
+      iApply (wp_wand with "(H2 HΓ2)"). iIntros (v) "[Hv HΓ3]".
+      iApply (wp_wand with "(Hv HA)"). iIntros (v') "HB".
+      iFrame "HΓ3 HB".
+    - wp_bind (subst_map vs e3).
+      iApply (wp_wand with "(H3 HΓ2)"). iIntros (v) "[Hv HΓ3]".
+      iApply (wp_wand with "(Hv HA)"). iIntros (v') "HB".
+      iFrame "HΓ3 HB".
   Qed.
 
   (** Universal Properties *)
@@ -242,280 +241,194 @@ Section properties.
     wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists M.
   Qed.
 
-  Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 x e1 e2 (C : lty Σ k → ltty Σ) B :
-    (Γ1 ⊨ e1 : lty_exist C ⫤ Γ2) -∗
-    (∀ Y, binder_insert x (C Y) Γ2 ⊨ e2 : B ⫤ Γ3) -∗
-    Γ1 ⊨ (let: x := e1 in e2) : B ⫤ binder_delete x Γ3.
+  Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 (x : string) e (C : lty Σ k → ltty Σ) A :
+    Γ1 !! x = Some (lty_exist C) →
+    (∀ X, binder_insert x (C X) Γ1 ⊨ e : A ⫤ Γ2) -∗
+    (Γ1 ⊨ e : A ⫤ Γ2).
   Proof.
-    iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1"=> /=.
-    wp_apply (wp_wand with "(He1 HΓ1)").
-    iIntros (v) "[HC HΓ2]".
-    iDestruct "HC" as (X) "HX".
-    wp_pures.
-    iDestruct (env_ltyped_insert _ _ x with "HX HΓ2") as "HΓ2".
-    iDestruct ("He2" with "HΓ2") as "He2'".
-    destruct x as [|x]; rewrite /= -?subst_map_insert //.
-    wp_apply (wp_wand with "He2'").
-    iIntros (w) "[HA2 HΓ3]".
-    iFrame.
-    iApply env_ltyped_delete=> //.
+    iIntros (Hx) "#He". iIntros (vs) "!> HΓ".
+    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HB HΓ]"; first done.
+    iDestruct ("HB") as (B) "HB".
+    iDestruct (env_ltyped_insert _ _ x with "HB HΓ") as "HΓ".
+    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
+    iApply (wp_wand with "(He HΓ)"). eauto.
   Qed.
 
   (** Mutable Reference properties *)
-  Definition alloc : val := λ: "init", ref "init".
-  Lemma ltyped_alloc A :
-    ⊢ ∅ ⊨ alloc : A → ref_mut A.
+  Lemma ltyped_alloc Γ1 Γ2 e A :
+    (Γ1 ⊨ e : A ⫤ Γ2) -∗
+    (Γ1 ⊨ ref e : ref_mut A ⫤ Γ2).
   Proof.
-    iIntros (vs) "!> HΓ /=". iApply wp_value.
-    iSplitL; last by iApply env_ltyped_empty.
-    iIntros "!>" (v) "Hv". rewrite /alloc. wp_pures.
+    iIntros "#He" (vs) "!> HΓ1 /=".
+    wp_bind (subst_map vs e).
+    iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv HΓ2]".
     wp_alloc l as "Hl".
-    iExists l, v. iSplit=> //.
-    iFrame "Hv Hl".
+    iFrame "HΓ2".
+    iExists l, v; iSplit=>//. iFrame "Hv Hl".
   Qed.
 
-  (* The intuition for the any is that the value is still there, but
-  it no longer holds any Iris resources. Just as in Rust, where a move
-  might turn into a memcpy, which leaves the original memory
-  unmodified, but moves the resources, in the sense that you can no
-  longer use the memory at the old location. *)
-  Definition load : val := λ: "r", (!"r", "r").
-  Lemma ltyped_load A :
-    ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut any.
+  Lemma ltyped_load Γ (x : string) A :
+    Γ !! x = Some (ref_mut A)%lty →
+    ⊢ Γ ⊨ ! x : A ⫤ <[x := (ref_mut (copy- A))%lty]> Γ.
   Proof.
-    iIntros (vs) "!> HΓ /=". iApply wp_value.
-    iSplitL; last by iApply env_ltyped_empty.
-    iIntros "!>" (v) "Hv". rewrite /load. wp_pures.
-    iDestruct "Hv" as (l w ->) "[Hl Hw]".
-    wp_load. wp_pures.
-    iExists w, #l. iSplit=> //. iFrame "Hw".
-    iExists l, w. iSplit=> //. iFrame "Hl".
-    by iModIntro.
+    iIntros (Hx vs) "!> HΓ".
+    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done.
+    simpl. rewrite Hv.
+    iDestruct "HA" as (l w ->) "[Hl Hw]".
+    wp_load.
+    iAssert (ltty_car (copy- A) w)%lty as "#HAm".
+    { iApply coreP_intro. iApply "Hw". }
+    iFrame "Hw".
+    iAssert (ltty_car (ref_mut (copy- A))%lty #l) with "[Hl]" as "HA".
+    { iExists l, w. iSplit=>//. iFrame "Hl HAm". }
+    iDestruct (env_ltyped_insert _ _ x with "HA HΓ") as "HΓ".
+    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
+    iFrame "HΓ".
   Qed.
 
-  (* TODO(COPY) *)
-  (* Lemma ltyped_load_copy A {copyA : LTyCopy A} : *)
-  (*   ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut A. *)
-  (* Proof. *)
-  (*   iIntros (vs) "!> HΓ /=". *)
-  (*   iApply wp_value. *)
-  (*   iIntros "!>" (v) "Hv". rewrite /load. wp_pures. *)
-  (*   iDestruct "Hv" as (l w ->) "[Hl #Hw]". *)
-  (*   wp_load. wp_pures. *)
-  (*   iExists w, #l. iSplit=> //. iFrame "Hw". *)
-  (*   iExists l, w. iSplit=> //. iFrame "Hl". *)
-  (*   by iModIntro. *)
-  (* Qed. *)
-
-  Definition store : val := λ: "r" "new", "r" <- "new";; "r".
-
-  Lemma ltyped_store A B :
-    ⊢ ∅ ⊨ store : ref_mut A → B ⊸ ref_mut B.
+  Lemma ltyped_store Γ Γ' (x : string) e A B :
+    Γ' !! x = Some (ref_mut A)%lty →
+    (Γ ⊨ e : B ⫤ Γ') -∗
+    Γ ⊨ x <- e : () ⫤ <[x := (ref_mut B)%lty]> Γ'.
   Proof.
-    iIntros (vs) "!> HΓ /=". iApply wp_value.
-    iSplitL; last by iApply env_ltyped_empty.
-    iIntros "!>" (v) "Hv". rewrite /store. wp_pures.
-    iDestruct "Hv" as (l old ->) "[Hl Hold]".
-    iIntros (new) "Hnew". wp_store.
-    iExists l, new. eauto with iFrame.
+    iIntros (Hx) "#He". iIntros (vs) "!> HΓ /=".
+    wp_bind (subst_map vs e).
+    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
+    iDestruct (env_ltyped_lookup with "HΓ'") as (w Hw) "[HA HΓ']"; first done.
+    rewrite Hw.
+    iDestruct "HA" as (l v' ->) "[Hl HA]".
+    wp_store. iSplitR; first done.
+    iAssert (ltty_car (ref_mut B)%lty #l) with "[Hl HB]" as "HB".
+    { iExists l, v. iSplit=>//. iFrame "Hl HB". }
+    iDestruct (env_ltyped_insert _ _ x with "HB HΓ'") as "HΓ'".
+    rewrite /binder_insert insert_delete (insert_id _ _ _ Hw).
+    iFrame "HΓ'".
   Qed.
 
   (** Weak Reference properties *)
-  Definition fetch_and_add : val := λ: "r" "inc", FAA "r" "inc".
-  Lemma ltyped_fetch_and_add :
-    ⊢ ∅ ⊨ fetch_and_add : ref_shr lty_int → lty_int → lty_int.
+  Lemma ltyped_upgrade_shared  Γ Γ' e A :
+    (Γ ⊨ e : ref_mut A ⫤ Γ') -∗
+    Γ ⊨ e : ref_shr A ⫤ Γ'.
   Proof.
-    iIntros (vs) "!> _ /=". iApply wp_value.
-    iSplitL; last by iApply env_ltyped_empty.
-    iIntros "!>" (r) "Hr".
-    iApply wp_fupd. rewrite /fetch_and_add; wp_pures.
-    iDestruct "Hr" as (l ->) "Hr".
-    iMod (fupd_mask_mono with "Hr") as "#Hr"; first done.
-    iIntros "!> !>" (inc) "Hinc". wp_pures.
-    iDestruct "Hinc" as %[k ->].
-    iInv (ref_shrN .@ l) as (n) "[>Hl >Hn]" "Hclose".
-    iDestruct "Hn" as %[m ->]. wp_faa.
-    iMod ("Hclose" with "[Hl]") as %_.
-    { iExists #(m + k). iFrame "Hl". by iExists (m + k)%Z. }
-    by iExists m.
+    iIntros "#He" (vs) "!> HΓ".
+    iApply wp_fupd.
+    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv HΓ']".
+    iDestruct "Hv" as (l w ->) "[Hl HA]".
+    iFrame "HΓ'".
+    iExists l.
+    iMod (inv_alloc (ref_shrN .@ l) _ (∃ v : val, l ↦ v ∗ ltty_car A v) with "[Hl HA]") as "Href".
+    { iExists w. iFrame "Hl HA". }
+    iModIntro.
+    by iFrame "Href".
   Qed.
 
-  (* TODO(COPY) *)
-  (* Lemma ltyped_ref_shr_load (A : lty Σ) {copyA : LTyCopy A} : *)
-  (*   ⊢ ∅ ⊨ load : ref_shr A → (A * ref_shr A). *)
-  (* Proof. *)
-  (*   iIntros (vs) "!> _ /=". iApply wp_value. iIntros "!>" (r) "Hr". *)
-  (*   iApply wp_fupd. rewrite /load; wp_pures. *)
-  (*   iDestruct "Hr" as (l ->) "Hr". *)
-  (*   iMod (fupd_mask_mono with "Hr") as "#Hr"; first done. *)
-  (*   wp_bind (!#l)%E. *)
-  (*   iInv (ref_shrN .@ l) as (v) "[>Hl #HA]" "Hclose". *)
-  (*   wp_load. *)
-  (*   iMod ("Hclose" with "[Hl HA]") as "_". *)
-  (*   { iExists v. iFrame "Hl HA". } *)
-  (*   iIntros "!>". wp_pures. iIntros "!>". *)
-  (*   iExists _, _. *)
-  (*   iSplit; first done. *)
-  (*   iFrame "HA". *)
-  (*   iExists _. *)
-  (*   iSplit; first done. *)
-  (*   by iFrame "Hr". *)
-  (* Qed. *)
-
-  Lemma ltyped_ref_shrstore A :
-    ⊢ ∅ ⊨ store : ref_shr A → A → ref_shr A.
+  Lemma ltyped_load_shared Γ Γ' e A :
+    (Γ ⊨ e : ref_shr A ⫤ Γ') -∗
+    Γ ⊨ ! e : copy- A ⫤ Γ'.
   Proof.
-    iIntros (vs) "!> _ /=". iApply wp_value.
-    iSplitL; last by iApply env_ltyped_empty.
-    iIntros "!>" (r) "Hr".
-    iApply wp_fupd. rewrite /store; wp_pures.
-    iDestruct "Hr" as (l ->) "#Hr".
-    iIntros "!> !>" (x) "HA". wp_pures.
-    wp_bind (_ <- _)%E.
-    iInv (ref_shrN .@ l) as (v) "[>Hl _]" "Hclose".
-    wp_store. iMod ("Hclose" with "[Hl HA]") as "_".
-    { iExists x. iFrame "Hl HA". }
-    iModIntro. wp_pures. iExists _. iSplit; first done. by iFrame "Hr".
+    iIntros "#He" (vs) "!> HΓ /=".
+    wp_bind (subst_map vs e).
+    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv HΓ]".
+    iDestruct "Hv" as (l ->) "#Hv".
+    iInv (ref_shrN .@ l) as (v) "[>Hl HA]" "Hclose".
+    wp_load.
+    iAssert (ltty_car (copy- A) v)%lty as "#HAm". { iApply coreP_intro. iApply "HA". }
+    iMod ("Hclose" with "[Hl HA]") as "_".
+    { iExists v. iFrame "Hl HA". }
+    iModIntro.
+    iFrame "HAm HΓ".
   Qed.
 
-  Section with_lock.
-    Context `{lockG Σ}.
-
-    (** Mutex properties *)
-    Definition mutexalloc : val := λ: "x", (newlock #(), ref "x").
-    Lemma ltyped_mutexalloc A :
-      ⊢ ∅ ⊨ mutexalloc : A → mutex A.
-    Proof.
-      iIntros (vs) "!> HΓ /=". iApply wp_value.
-      iSplitL; last by iApply env_ltyped_empty.
-      iIntros "!>" (v) "Hv". rewrite /mutexalloc. wp_pures.
-      wp_alloc l as "Hl".
-      wp_bind (newlock _).
-      set (N := nroot .@ "makelock").
-      iAssert (∃ inner, l ↦ inner ∗ ltty_car A inner)%I with "[Hl Hv]" as "Hlock".
-      { iExists v. iFrame "Hl Hv". }
-      wp_apply (newlock_spec with "Hlock").
-      iIntros (lk γ) "Hlock".
-      wp_pures. iExists γ, l, lk. iSplit=> //.
-    Qed.
-
-    Definition mutexacquire : val := λ: "x", acquire (Fst "x");; (! (Snd "x"), "x").
-    Lemma ltyped_mutexacquire A :
-      ⊢ ∅ ⊨ mutexacquire : mutex A → A * mutexguard A.
-    Proof.
-      iIntros (vs) "!> HΓ /=". iApply wp_value.
-      iSplitL; last by iApply env_ltyped_empty.
-      iIntros "!>" (m) "Hm". rewrite /mutexacquire. wp_pures.
-      iDestruct "Hm" as (γ l lk ->) "Hlock".
-      iMod (fupd_mask_mono with "Hlock") as "#Hlock"; first done.
-      wp_bind (acquire _).
-      wp_apply (acquire_spec with "Hlock").
-      iIntros "[Hlocked Hinner]".
-      wp_pures.
-      iDestruct "Hinner" as (v) "[Hl HA]".
-      wp_load. wp_pures.
-      iExists v, (lk, #l)%V. iSplit=> //.
-      iFrame "HA".
-      iExists γ, l, lk, v. iSplit=> //.
-      by iFrame "Hl Hlocked Hlock".
-    Qed.
+  Lemma ltyped_store_shared Γ1 Γ2 Γ3 e1 e2 A :
+    (Γ1 ⊨ e2 : A ⫤ Γ2) -∗
+    (Γ2 ⊨ e1 : ref_shr A ⫤ Γ3) -∗
+    (Γ1 ⊨ e1 <- e2 : () ⫤ Γ3).
+  Proof.
+    iIntros "#H1 #H2" (vs) "!> HΓ1 /=".
+    wp_bind (subst_map vs e2).
+    iApply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
+    wp_bind (subst_map vs e1).
+    iApply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw HΓ3]".
+    iDestruct "Hw" as (l ->) "#Hw".
+    iInv (ref_shrN .@ l) as (?) "[>Hl HA]" "Hclose".
+    wp_store.
+    iMod ("Hclose" with "[Hl Hv]") as "_".
+    { iExists v. iFrame "Hl Hv". }
+    iModIntro. iSplit=>//.
+  Qed.
 
-    Definition mutexrelease : val :=
-      λ: "inner" "guard", Snd "guard" <- "inner";; release (Fst "guard");; "guard".
-    Lemma ltyped_mutexrelease A :
-      ⊢ ∅ ⊨ mutexrelease : A → mutexguard A ⊸ mutex A.
-    Proof.
-      iIntros (vs) "!> HΓ /=". iApply wp_value.
-      iSplitL; last by iApply env_ltyped_empty.
-      iIntros "!>" (w1) "Hw1". rewrite /mutexrelease. wp_pures.
-      iIntros (w2) "Hw2". wp_pures.
-      iDestruct "Hw2" as (γ l lk inner ->) "[#Hlock [Hlocked Hinner]]".
-      wp_store.
-      iAssert (∃ inner : val, l ↦ inner ∗ ltty_car A inner)%I
-        with "[Hinner Hw1]" as "Hinner".
-      { iExists w1. iFrame "Hinner Hw1". }
-      wp_bind (release _).
-      wp_apply (release_spec γ _ (∃ inner, l ↦ inner ∗ ltty_car A inner)%I
-                  with "[Hlocked Hinner]").
-      { iFrame "Hlock Hlocked".
-        iDestruct "Hinner" as (v) "[Hl HA]". eauto with iFrame. }
-      iIntros "_". wp_pures.
-      iExists γ, l, lk. iSplit=> //.
-    Qed.
-  End with_lock.
+  Lemma ltyped_fetch_and_add_shared Γ1 Γ2 Γ3 e1 e2 :
+    (Γ1 ⊨ e2 : lty_int ⫤ Γ2) -∗
+    (Γ2 ⊨ e1 : ref_shr lty_int ⫤ Γ3) -∗
+    (Γ1 ⊨ FAA e1 e2 : lty_int ⫤ Γ3).
+  Proof.
+    iIntros "#H1 #H2" (vs) "!> HΓ1 /=".
+    wp_bind (subst_map vs e2).
+    iApply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
+    wp_bind (subst_map vs e1).
+    iApply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw HΓ3]".
+    iDestruct "Hw" as (l ->) "#Hw".
+    iInv (ref_shrN .@ l) as (w) "[Hl >Hn]" "Hclose".
+    iDestruct "Hn" as %[k ->].
+    iDestruct "Hv" as %[n ->].
+    wp_faa.
+    iMod ("Hclose" with "[Hl]") as %_.
+    { iExists #(k + n). iFrame "Hl". by iExists (k + n)%Z. }
+    iModIntro. iFrame "HΓ3". by iExists k.
+  Qed.
 
   Section with_spawn.
     Context `{spawnG Σ}.
 
     (** Parallel composition properties *)
-    Definition parallel : val := λ: "e1" "e2", par "e1" "e2".
-
-    Lemma ltyped_parallel A B :
-      ⊢ ∅ ⊨ parallel : (() ⊸ A) → (() ⊸ B) ⊸ (A * B).
+    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') -∗
+      Γ ⊨ e1 ||| e2 : A * B ⫤ Γ'.
     Proof.
-      iIntros (vs) "!> HΓ /=". iApply wp_value.
-      iSplitL; last by iApply env_ltyped_empty.
-      iIntros "!>" (fa) "Hfa". rewrite /parallel. wp_pures.
-      iIntros (fb) "Hfb". wp_pures.
-      wp_apply (par_spec (ltty_car A) (ltty_car B) with "[Hfa] [Hfb]").
-      - by wp_apply "Hfa".
-      - by wp_apply "Hfb".
-      - iIntros (v1 v2) "[HA HB] !>". iExists v1, v2. eauto with iFrame.
+      iIntros "#Hsplit #Hsplit' #H1 #H2" (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").
+      - iApply ("H2" with "HΓ2").
+      - iIntros (v1 v2) "[[HA HΓ1'] [HB HΓ2']]".
+        iModIntro. iSplitL "HA HB".
+        + iExists v1, v2. iSplit=>//. iFrame "HA HB".
+        + iApply "Hsplit'". iFrame "HΓ1' HΓ2'".
     Qed.
   End with_spawn.
 
   Section with_chan.
     Context `{chanG Σ}.
 
-    Definition chanalloc : val := λ: "u", let: "cc" := new_chan #() in "cc".
-    Lemma ltyped_chanalloc S :
-      ⊢ ∅ ⊨ chanalloc : () → (chan S * chan (lty_dual S)).
-    Proof.
-      iIntros (vs) "!> HΓ /=". iApply wp_value.
-      iSplitL; last by iApply env_ltyped_empty.
-      iIntros "!>" (u) ">->". rewrite /chanalloc. wp_pures.
-      wp_apply (new_chan_spec with "[//]"); iIntros (c1 c2) "Hp".
-      iDestruct "Hp" as "[Hp1 Hp2]". wp_pures.
-      iExists c1, c2. iSplit=> //. iSplitL "Hp1"; by iModIntro.
-    Qed.
-
-    Definition chansend : val := λ: "chan" "val", send "chan" "val";; "chan".
-    Lemma ltyped_chansend A S :
-      ⊢ ∅ ⊨ chansend : chan (<!!> TY A; S) → A ⊸ chan S.
+    Lemma ltyped_new_chan S :
+      ⊢ ∅ ⊨ new_chan : () → (chan S * chan (lty_dual S)).
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
       iSplitL; last by iApply env_ltyped_empty.
-      iIntros "!>" (c) "Hc". rewrite /chansend. wp_pures.
-      iIntros (w) "Hw". wp_pures.
-      wp_send with "[$Hw]". wp_pures. iFrame "Hc".
+      iIntros "!>" (u) ">->".
+      iApply (new_chan_spec with "[//]"); iIntros (c1 c2) "!> [Hp1 Hp2]".
+      iExists c1, c2. iSplit=>//. iFrame "Hp1 Hp2".
     Qed.
 
     Lemma ltyped_send Γ Γ' (x : string) e A S :
-      (Γ ⊨ e : A ⫤ <[x:=(chan (<!!> TY A; S))%lty]> Γ') -∗
+      Γ' !! x = Some (chan (<!!> TY A; S))%lty →
+      (Γ ⊨ e : A ⫤ Γ') -∗
       Γ ⊨ send x e : () ⫤ <[x:=(chan S)%lty]> Γ'.
     Proof.
-      iIntros "#He !>" (vs) "HΓ"=> /=.
+      iIntros (Hx) "#He !>". iIntros (vs) "HΓ"=> /=.
       wp_bind (subst_map vs e).
       iApply (wp_wand with "(He HΓ)"); iIntros (v) "[HA HΓ']".
       iDestruct (env_ltyped_lookup with "HΓ'") as (v' Heq) "[Hc HΓ']".
-      { by apply lookup_insert. }
+      { by apply Hx. }
       rewrite Heq.
       wp_send with "[HA //]".
       iSplitR; first done.
       iDestruct (env_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ'")
         as "HΓ'"=> /=.
-      by rewrite insert_delete insert_insert (insert_id vs).
-    Qed.
-
-    Definition chanrecv : val := λ: "chan", (recv "chan", "chan").
-    Lemma ltyped_chanrecv A S :
-      ⊢ ∅ ⊨ chanrecv : chan (<??> TY A; S) → A * chan S.
-    Proof.
-      iIntros (vs) "!> HΓ /=". iApply wp_value.
-      iSplitL; last by iApply env_ltyped_empty.
-      iIntros "!>" (c) "Hc". rewrite /chanrecv. wp_pures.
-      wp_recv (v) as "HA". wp_pures.
-      iExists v, c. eauto with iFrame.
+      by rewrite insert_delete (insert_id vs).
     Qed.
 
     Lemma iProto_le_lmsg_texist {kt : ktele Σ} (m : ltys Σ kt → iMsg Σ) :
@@ -553,31 +466,17 @@ Section properties.
     Qed.
 
     Lemma ltyped_recv Γ (x : string) A S :
-      ⊢ <[x := (chan (<??> TY A; S))%lty]> Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
+      Γ !! x = Some (chan (<??> TY A; S))%lty →
+      ⊢ Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
     Proof.
-      iIntros "!>" (vs) "HΓ"=> /=.
+      iIntros (Hx) "!>". iIntros (vs) "HΓ"=> /=.
       iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".
-      { by apply lookup_insert. }
+      { by apply Hx. }
       rewrite Heq.
       wp_recv (v) as "HA".
       iSplitL "HA"; first done.
       iDestruct (env_ltyped_insert _ _ x (chan _) _ with "[Hc //] HΓ") as "HΓ"=> /=.
-      by rewrite insert_delete !insert_insert (insert_id vs).
-    Qed.
-
-    Definition chanselect : val := λ: "c" "i", send "c" "i";; "c".
-    Lemma ltyped_chanselect Γ (c : val) (i : Z) S Ss :
-      Ss !! i = Some S →
-      (Γ ⊨ c : chan (lty_select Ss)) -∗
-      Γ ⊨ chanselect c #i : chan S.
-    Proof.
-      iIntros (Hin) "#Hc !>".
-      iIntros (vs) "H /=".
-      rewrite /chanselect.
-      iMod (wp_value_inv with "(Hc H)") as "[Hc' HΓ]".
-      wp_send with "[]"; [by eauto|].
-      rewrite (lookup_total_correct Ss i S)=> //.
-      wp_pures. iFrame.
+      by rewrite insert_delete (insert_id vs).
     Qed.
 
     Definition select : val := λ: "c" "i", send "c" "i".
@@ -600,6 +499,45 @@ Section properties.
       by rewrite lookup_total_alt Hin.
     Qed.
 
+    Fixpoint lty_arr_list (As : list (ltty Σ)) (B : ltty Σ) : ltty Σ :=
+      match As with
+      | [] => B
+      | A :: As => A ⊸ lty_arr_list As B
+      end.
+
+    Lemma lty_arr_list_spec_step A As (e : expr) B ws y i :
+      (∀ v, ltty_car A v -∗
+        WP subst_map (<[y+:+pretty i:=v]> ws)
+          (switch_lams y (S i) (length As) e) {{ ltty_car (lty_arr_list As B) }}) -∗
+      WP subst_map ws (switch_lams y i (S (length As)) e)
+        {{ ltty_car (lty_arr_list (A :: As) B) }}.
+    Proof.
+      iIntros "H". wp_pures. iIntros (v) "HA".
+      iDestruct ("H" with "HA") as "H".
+      rewrite subst_map_insert.
+      wp_apply "H".
+    Qed.
+
+    Lemma lty_arr_list_spec As (e : expr) B ws y i n :
+      n = length As →
+      (∀ vs, ([∗ list] A;v ∈ As;vs, ltty_car A v) -∗
+            WP subst_map (map_string_seq y i vs ∪ ws) e {{ ltty_car B }}) -∗
+      WP subst_map ws (switch_lams y i n e) {{ ltty_car (lty_arr_list As B) }}.
+    Proof.
+      iIntros (Hlen) "H".
+      iInduction As as [|A As] "IH" forall (ws i e n Hlen); simplify_eq/=.
+      - iDestruct ("H" $! [] with "[$]") as "H"=> /=.
+        by rewrite left_id_L.
+      - iApply lty_arr_list_spec_step. iIntros (v) "HA".
+        iApply ("IH" with "[//]"). iIntros (vs) "HAs".
+        iSpecialize ("H" $! (v::vs)); simpl.
+        do 2 rewrite insert_union_singleton_l.
+        rewrite (map_union_comm ({[y +:+ pretty i := v]})); last first.
+        { apply map_disjoint_singleton_l_2.
+          apply lookup_map_string_seq_None_lt. eauto. }
+        rewrite assoc_L. iApply ("H" with "[$HA $HAs]").
+    Qed.
+
     Definition chanbranch (xs : list Z) : val := λ: "c",
       switch_lams "f" 0 (length xs) $
       let: "y" := recv "c" in