diff --git a/theories/logrel/environments.v b/theories/logrel/environments.v
index 02d02cbc1efed3c669e68d2707ffd779367ca7aa..80e6f98ff70cb49e9d108b5b49292e497a43dfb0 100644
--- a/theories/logrel/environments.v
+++ b/theories/logrel/environments.v
@@ -12,181 +12,188 @@ to the syntactic typing rules that are typically found in substructural type
 systems. *)
 From actris.logrel Require Export term_types subtyping.
 From iris.proofmode Require Import tactics.
-
-Notation "<![ b := x ]!>" :=
-  (binder_insert b x%lty) (at level 5, right associativity).
-
-Definition env_ltyped {Σ} (Γ : gmap string (ltty Σ))
-    (vs : gmap string val) : iProp Σ :=
-  ([∗ map] i ↦ A ∈ Γ, ∃ v, ⌜vs !! i = Some v⌝ ∗ ltty_car A v)%I.
-
-Definition env_split {Σ} (Γ Γ1 Γ2 : gmap string (ltty Σ)) : iProp Σ :=
-  (■ ∀ vs, env_ltyped Γ vs ∗-∗ (env_ltyped Γ1 vs ∗ env_ltyped Γ2 vs))%I.
-
-Definition env_copy {Σ} (Γ Γ' : gmap string (ltty Σ)) : iProp Σ :=
-  (■ ∀ vs, env_ltyped Γ vs -∗ □ env_ltyped Γ' vs)%I.
+From iris.algebra Require Export list.
+
+Inductive env_item Σ := EnvItem {
+  env_item_name : string;
+  env_item_type : ltty Σ;
+}.
+Add Printing Constructor env_item.
+Arguments EnvItem {_} _ _.
+Arguments env_item_name {_} _.
+Arguments env_item_type {_} _.
+Instance: Params (@EnvItem) 2 := {}.
+Instance: Params (@env_item_type) 1 := {}.
+
+Section env_item_ofe.
+  Context {Σ : gFunctors}.
+  Instance env_item_equiv : Equiv (env_item Σ) := λ xA1 xA2,
+    env_item_name xA1 = env_item_name xA2 ∧ env_item_type xA1 ≡ env_item_type xA2.
+  Instance env_item_dist : Dist (env_item Σ) := λ n xA1 xA2,
+    env_item_name xA1 = env_item_name xA2 ∧ env_item_type xA1 ≡{n}≡ env_item_type xA2.
+  Lemma env_item_ofe_mixin : OfeMixin (env_item Σ).
+  Proof.
+    by apply (iso_ofe_mixin (A:=prodO (leibnizO string) (lttyO Σ))
+      (λ xA, (env_item_name xA, env_item_type xA))).
+  Qed.
+  Canonical Structure env_itemO := OfeT (env_item Σ) env_item_ofe_mixin.
+  Global Instance env_item_type_ne : NonExpansive (@env_item_type Σ).
+  Proof. by intros n ?? [??]. Qed.
+  Global Instance env_item_type_proper : Proper ((≡) ==> (≡)) (@env_item_type Σ).
+  Proof. by intros ?? [??]. Qed.
+End env_item_ofe.
+
+Notation env Σ := (list (env_item Σ)).
+
+Definition env_filter_eq {Σ} (x : binder) : env Σ → env Σ :=
+  filter (λ xA, x = BNamed (env_item_name xA)).
+Definition env_filter_ne {Σ} (x : binder) : env Σ → env Σ :=
+  filter (λ xA, x ≠ BNamed (env_item_name xA)).
+
+Arguments env_filter_eq _ !_ !_ / : simpl nomatch.
+Arguments env_filter_ne _ !_ !_ / : simpl nomatch.
+(** TODO: Move to std++, together with some lemmas about filter that can be
+factored out. *)
+Arguments filter _ _ _ _ _ !_ / : simpl nomatch.
+
+Definition env_cons {Σ} (b : binder) (A : ltty Σ) (Γ : env Σ) : env Σ :=
+  if b is BNamed x then EnvItem x A :: env_filter_ne x Γ else Γ.
+
+Definition env_ltyped {Σ} (vs : gmap string val) (Γ : env Σ) : iProp Σ :=
+  ([∗ list] iA ∈ Γ, ∃ v,
+    ⌜vs !! env_item_name iA = Some v⌝ ∗ ltty_car (env_item_type iA) v)%I.
+Instance: Params (@env_ltyped) 2 := {}.
+
+Definition env_le {Σ} (Γ1 Γ2 : env Σ) : iProp Σ :=
+  tc_opaque (■ ∀ vs, env_ltyped vs Γ1 -∗ env_ltyped vs Γ2)%I.
+Instance: Params (@env_le) 1 := {}.
 
 Section env.
   Context {Σ : gFunctors}.
   Implicit Types A : ltty Σ.
-  Implicit Types Γ : gmap string (ltty Σ).
+  Implicit Types Γ : env Σ.
 
-  Lemma env_ltyped_empty vs : ⊢@{iPropI Σ} env_ltyped ∅ vs.
-  Proof. by iApply big_sepM_empty. Qed.
-
-  Lemma env_ltyped_lookup Γ vs x A :
-    Γ !! x = Some A →
-    env_ltyped Γ vs -∗
-    ∃ v, ⌜ vs !! x = Some v ⌝ ∗ ltty_car A v ∗ env_ltyped (delete x Γ) vs.
+  (** env_filter *)
+  Lemma env_filter_eq_perm Γ x : Γ ≡ₚ env_filter_eq x Γ ++ env_filter_ne x Γ.
   Proof.
-    iIntros (HΓx) "HΓ".
-    iPoseProof (big_sepM_delete with "HΓ") as "[HA H]"; eauto.
-    iDestruct "HA" as (v) "HA"; eauto with iFrame.
+    rewrite /env_filter_eq /env_filter_ne.
+    induction Γ as [|[y A] Γ IH]; simpl; [done|].
+    rewrite filter_cons. case_decide.
+    - rewrite filter_cons_False /=; last naive_solver. by rewrite -IH.
+    - rewrite filter_cons_True /=; last naive_solver.
+      by rewrite -Permutation_middle -IH.
   Qed.
-
-  Lemma env_ltyped_insert Γ vs x A v :
-    ltty_car A v -∗
-    env_ltyped Γ vs -∗
-    env_ltyped (<![x:=A]!> Γ) (<![x:=v]!> vs).
+  Lemma env_filter_eq_perm' Γ Γ' x :
+    env_filter_eq x Γ = Γ' →
+    Γ ≡ₚ Γ' ++ env_filter_ne x Γ.
+  Proof. intros <-. apply env_filter_eq_perm. Qed.
+
+  Lemma env_filter_ne_anon Γ : env_filter_ne BAnon Γ = Γ.
+  Proof. induction Γ as [|[y A] Γ IH]; by f_equal/=. Qed.
+
+  Lemma elem_of_env_filter_ne Γ x y B :
+    EnvItem y B ∈ env_filter_ne x Γ → x ≠ y.
+  Proof. intros ?%elem_of_list_filter. naive_solver. Qed.
+
+  Lemma env_filter_ne_cons Γ (x : string) A :
+    env_filter_ne x (EnvItem x A :: Γ) = env_filter_ne x Γ.
+  Proof. rewrite /env_filter_ne filter_cons_False; naive_solver. Qed.
+  Lemma env_filter_ne_cons_ne Γ x y A :
+    x ≠ BNamed y →
+    env_filter_ne x (EnvItem y A :: Γ) = EnvItem y A :: env_filter_ne x Γ.
+  Proof. intros. rewrite /env_filter_ne filter_cons_True; naive_solver. Qed.
+
+  (** env typing *)
+  Global Instance env_ltyped_Permutation vs :
+    Proper ((≡ₚ) ==> (⊣⊢)) (@env_ltyped Σ vs).	
+  Proof. intros Γ Γ' HΓ. by rewrite /env_ltyped HΓ. Qed.
+  Global Instance env_ltyped_ne vs : NonExpansive (@env_ltyped Σ vs).
   Proof.
-    destruct x as [|x]=> /=; first by auto.
-    iIntros "HA HΓ".
-    rewrite /env_ltyped.
-    set Γ' := <[x:=A]> Γ.
-    assert (Hx: Γ' !! x = Some A).
-    { apply lookup_insert. }
-    iApply (big_sepM_delete _ _ _ _ Hx).
-    iSplitL "HA".
-    { iExists v. rewrite lookup_insert. auto. }
-    assert (Hsub: delete x Γ' ⊆ Γ).
-    { rewrite delete_insert_delete. apply delete_subseteq. }
-    iPoseProof (big_sepM_subseteq _ _ _ Hsub with "HΓ") as "HΓ".
-    iApply (big_sepM_mono with "HΓ"). simpl.
-    iIntros (y B Hy) "HB".
-    iDestruct "HB" as (w Hw) "HB".
-    iExists w. iFrame. iPureIntro.
-    apply lookup_delete_Some in Hy.
-    destruct Hy as [Hxy _].
-    by rewrite -Hw lookup_insert_ne.
+    intros n Γ Γ' HΓ. rewrite /env_ltyped.
+    apply big_opL_gen_proper_2; [done|apply _|]. intros k.
+    assert (Γ !! k ≡{n}≡ Γ' !! k) as HΓk by (by rewrite HΓ).
+    case: HΓk=> // -[x1 A1] [x2 A2] [/= -> ?]. by repeat f_equiv.
   Qed.
+  Global Instance env_ltyped_proper vs : Proper ((≡) ==> (≡)) (@env_ltyped Σ vs).
+  Proof. apply (ne_proper _). Qed.
 
-  Lemma env_ltyped_delete Γ x v vs :
-    env_ltyped Γ (<[x:=v]> vs) -∗
-    env_ltyped (delete x Γ) vs.
-  Proof.
-    iIntros "HΓ".
-    rewrite /env_ltyped. destruct (Γ !! x) as [A|] eqn:?.
-    { iDestruct (big_sepM_delete with "HΓ") as "[HA HΓ]"; first done.
-      iDestruct "HA" as (v' ?) "HA"; simplify_map_eq.
-      iApply (big_sepM_impl with "HΓ").
-      iIntros "!>" (y B ?). iDestruct 1 as (v'' ?) "HB".
-      destruct (decide (x = y)); simplify_map_eq; eauto. }
-    rewrite delete_notin //. iApply (big_sepM_impl with "HΓ").
-    iIntros "!>" (y B ?). iDestruct 1 as (v' ?) "HB"; simplify_map_eq; eauto.
-  Qed.
+  Lemma env_ltyped_nil vs : ⊢@{iPropI Σ} env_ltyped vs [].
+  Proof. done. Qed.
 
-  Lemma env_split_id_l Γ : ⊢ env_split Γ ∅ Γ.
-  Proof.
-    iIntros "!>" (vs).
-    iSplit; [iIntros "$" | iIntros "[_ $]"]; iApply env_ltyped_empty.
-  Qed.
-  Lemma env_split_id_r Γ : ⊢ env_split Γ Γ ∅.
-  Proof.
-    iIntros "!>" (vs).
-    iSplit; [iIntros "$" | iIntros "[$ _]"]; iApply env_ltyped_empty.
-  Qed.
+  Lemma env_ltyped_app Γ1 Γ2 vs :
+    env_ltyped vs (Γ1 ++ Γ2) ⊣⊢ env_ltyped vs Γ1 ∗ env_ltyped vs Γ2.
+  Proof. apply big_opL_app. Qed.
 
-  Lemma env_split_empty : ⊢@{iPropI Σ} env_split ∅ ∅ ∅.
+  Lemma env_ltyped_cons Γ vs x A : 
+    env_ltyped vs (EnvItem x A :: Γ) ⊣⊢ ∃ v,
+    ⌜vs !! x = Some v⌝ ∗ ltty_car A v ∗ env_ltyped vs Γ.
   Proof.
-    iIntros "!>" (vs).
-    iSplit; [iIntros "HΓ" | iIntros "[HΓ1 HΓ2]"]; auto.
+    iSplit; [by iIntros "[HA $]"|].
+    iDestruct 1 as (v ?) "[HA $]"; eauto.
   Qed.
 
-  (* TODO: Get rid of side condition that x does not appear in Γ1 *)
-  Lemma env_split_left Γ Γ1 Γ2 x A:
-    Γ !! x = None → Γ1 !! x = None →
-    env_split Γ Γ1 Γ2 -∗
-    env_split (<[x := A]> Γ) (<[x := A]> Γ1) Γ2.
+  Lemma env_ltyped_insert Γ vs x A v :
+    ltty_car A v -∗
+    env_ltyped vs (env_filter_ne x Γ) -∗
+    env_ltyped (binder_insert x v vs) (env_cons x A Γ).
   Proof.
-    iIntros (HΓx HΓ2x) "#Hsplit !>". iIntros (vs).
-    iSplit.
-    - iIntros "HΓ".
-      iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption.
-      iDestruct ("Hsplit" with "HΓ") as "[HΓ1 $]".
-      iApply (big_sepM_insert_2 with "[Hv]"); simpl; eauto.
-    - iIntros "[HΓ1 HΓ2]".
-      iPoseProof (big_sepM_insert with "HΓ1") as "[Hv HΓ1]"; first by assumption.
-      iApply (big_sepM_insert_2 with "[Hv]")=> //.
-      iApply "Hsplit". iFrame "HΓ1 HΓ2".
+    iIntros "HA HΓ".
+    destruct x as [|x]; simpl; [rewrite env_filter_ne_anon; auto|].
+    iApply env_ltyped_cons. iExists _; iSplit; [by rewrite lookup_insert|].
+    iFrame "HA". iApply (big_sepL_impl with "HΓ").
+    iIntros "!>" (k [j B] ?%elem_of_list_lookup_2%elem_of_env_filter_ne).
+    iDestruct 1 as (w ?) "HB". iExists w. iIntros "{$HB} !%".
+    apply lookup_insert_Some; naive_solver.
   Qed.
 
-  Lemma env_split_comm Γ Γ1 Γ2:
-    env_split Γ Γ1 Γ2 -∗ env_split Γ Γ2 Γ1.
+  Lemma env_ltyped_delete Γ x v vs :
+    env_ltyped (binder_insert x v vs) Γ -∗
+    env_ltyped vs (env_filter_ne x Γ).
   Proof.
-    iIntros "#Hsplit" (vs) "!>".
-    iSplit.
-    - iIntros "HΓ". by iDestruct ("Hsplit" with "HΓ") as "[$ $]".
-    - iIntros "[HΓ1 HΓ2]". iApply "Hsplit". iFrame.
+    rewrite {1}(env_filter_eq_perm Γ x) env_ltyped_app. iIntros "[_ HΓ]".
+    iApply (big_sepL_impl with "HΓ").
+    iIntros "!>" (k [j B] ?%elem_of_list_lookup_2%elem_of_env_filter_ne).
+    iDestruct 1 as (w Hx) "HB". simpl in *. iExists w. iIntros "{$HB} !%".
+    destruct x as [|x]; simplify_eq/=; auto.
+    revert Hx. rewrite lookup_insert_Some. naive_solver.
   Qed.
 
-  (* TODO: Get rid of side condition that x does not appear in Γ2 *)
-  Lemma env_split_right Γ Γ1 Γ2 x A:
-    Γ !! x = None → Γ2 !! x = None →
-    env_split Γ Γ1 Γ2 -∗
-    env_split (<[x := A]> Γ) Γ1 (<[x := A]> Γ2).
+  (** Environment subtyping *)
+  Global Instance env_le_plain Γ1 Γ2 : Plain (env_le Γ1 Γ2).
+  Proof. rewrite /env_le /=. apply _. Qed.
+
+  Global Instance env_le_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡)) (@env_le Σ).
   Proof.
-    iIntros (HΓx HΓ2x) "Hsplit".
-    iApply env_split_comm. iApply env_split_left=> //.
-    by iApply env_split_comm.
+    intros Γ1 Γ1' HΓ1 Γ2 Γ2' HΓ2. rewrite /env_le /=.
+    setoid_rewrite HΓ1; by setoid_rewrite HΓ2.
   Qed.
-
-  (* TODO: Get rid of side condition that x does not appear in Γ *)
-  Lemma env_split_copyable Γ Γ1 Γ2 (x : string) A:
-    Γ !! x = None → Γ1 !! x = None → Γ2 !! x = None →
-    lty_copyable A -∗
-    env_split Γ Γ1 Γ2 -∗
-    env_split (<[x:=A]> Γ) (<[x:=A]> Γ1) (<[x:=A]> Γ2).
+  Global Instance env_le_ne : NonExpansive2 (@env_le Σ).
+  Proof. solve_proper. Qed.
+  Global Instance env_le_proper : Proper ((≡) ==> (≡) ==> (≡)) (@env_le Σ).
+  Proof. apply (ne_proper_2 _). Qed.
+
+  Lemma env_le_refl Γ : ⊢ env_le Γ Γ.
+  Proof. iIntros (vs); auto. Qed.
+  Lemma env_le_trans Γ1 Γ2 Γ3 : env_le Γ1 Γ2 -∗ env_le Γ2 Γ3 -∗ env_le Γ1 Γ3.
   Proof.
-    iIntros (HΓx HΓ1x HΓ2x) "#Hcopy #Hsplit". iIntros (vs) "!>".
-    iSplit.
-    - iIntros "HΓ".
-      iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption.
-      iDestruct "Hv" as (v ?) "HAv2".
-      iDestruct ("Hcopy" with "HAv2") as "#HAv".
-      iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
-      iSplitL "HΓ1"; iApply big_sepM_insert_2; simpl; eauto.
-    - iIntros "[HΓ1 HΓ2]".
-      iPoseProof (big_sepM_insert with "HΓ1") as "[Hv HΓ1]"; first by assumption.
-      iPoseProof (big_sepM_insert with "HΓ2") as "[_ HΓ2]"; first by assumption.
-      iApply (big_sepM_insert_2 with "[Hv]")=> //.
-      iApply "Hsplit". iFrame "HΓ1 HΓ2".
+    rewrite /env_le /=.
+    iIntros "#H1 #H2 !>" (vs) "Hvs". iApply "H2". by iApply "H1".
   Qed.
-
-  Lemma env_copy_empty : ⊢@{iPropI Σ} env_copy ∅ ∅.
-  Proof. iIntros (vs) "!> _ !> ". by rewrite /env_ltyped. Qed.
-
-  Lemma env_copy_extend x A Γ Γ' :
-    Γ !! x = None →
-    env_copy Γ Γ' -∗
-    env_copy (<[x:=A]> Γ) Γ'.
+  Lemma env_le_nil Γ : ⊢ env_le Γ [].
+  Proof. iIntros (vs) "!> _". iApply env_ltyped_nil. Qed.
+  Lemma env_le_cons x Γ1 Γ2 A1 A2 :
+    A1 <: A2 -∗ env_le Γ1 Γ2 -∗ env_le (EnvItem x A1 :: Γ1) (EnvItem x A2 :: Γ2).
   Proof.
-    iIntros (HΓ) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
-    iDestruct (big_sepM_insert with "Hvs") as "[_ Hvs]"; first by assumption.
-    iApply ("Hcopy" with "Hvs").
+    rewrite /env_le /=. iIntros "#H #H' !>" (vs) "Hvs".
+    iDestruct (env_ltyped_cons with "Hvs") as (v ?) "[Hv Hvs]".
+    iApply env_ltyped_cons. iExists _; iSplit; [done|].
+    iSplitL "Hv"; [by iApply "H"|by iApply "H'"].
   Qed.
-
-  Lemma env_copy_extend_copyable x A Γ Γ' :
-    Γ !! x = None →
-    Γ' !! x = None →
-    lty_copyable A -∗
-    env_copy Γ Γ' -∗
-    env_copy (<[x:=A]> Γ) (<[x:=A]> Γ').
+  Lemma env_le_app Γ1 Γ2 Γ1' Γ2' :
+    env_le Γ1 Γ2 -∗ env_le Γ1' Γ2' -∗ env_le (Γ1 ++ Γ1') (Γ2 ++ Γ2').
   Proof.
-    iIntros (HΓx HΓ'x) "#HcopyA #Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
-    iDestruct (big_sepM_insert with "Hvs") as "[HA Hvs]"; first done.
-    iDestruct ("Hcopy" with "Hvs") as "#Hvs'".
-    iDestruct "HA" as (v ?) "HA2".
-    iDestruct ("HcopyA" with "HA2") as "#HA".
-    iIntros "!>". iApply big_sepM_insert; first done. iSplitL; eauto.
+    rewrite /env_le /=. iIntros "#H #H' !>" (vs) "Hvs".
+    iDestruct (env_ltyped_app with "Hvs") as "[Hvs1 Hvs2]".
+    iApply env_ltyped_app. iSplitL "Hvs1"; [by iApply "H"|by iApply "H'"].
   Qed.
 End env.
diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index 1bf752315342ee3a4d3cbd3e9eb02faa7bd66324..93ac949cf57726a2f7b2c7688584c1adafa1fcfc 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -123,11 +123,10 @@ Section double.
   Qed.
 
   Lemma prog_typed :
-    ⊢ ∅ ⊨ prog : chan (<??> TY lty_int; <??> TY lty_int; END) ⊸ lty_int * lty_int.
+    ⊢ [] ⊨ prog : chan (<??> TY lty_int; <??> TY lty_int; END) ⊸ lty_int * lty_int.
   Proof.
     iIntros (vs) "!> HΓ /=".
-    iApply wp_value.
-    iSplitL; last by iApply env_ltyped_empty.
+    iApply wp_value. iSplitL; last by iApply env_ltyped_nil.
     iIntros (c) "Hc".
     iApply (wp_prog (λ v1 v2, ltty_car lty_int v1 ∗ ltty_car lty_int v2)%I with "[Hc]").
     { iApply (iProto_mapsto_le _ (lsty_car (<??> TY lty_int; <??> TY lty_int; END)) with "Hc").
diff --git a/theories/logrel/examples/mapper.v b/theories/logrel/examples/mapper.v
index a6c0c55447c2d9e215f6a23bd660b43ae52b9c26..624a82d946b6392146ef2d4dc84c848bbbac1696 100644
--- a/theories/logrel/examples/mapper.v
+++ b/theories/logrel/examples/mapper.v
@@ -1,7 +1,7 @@
-From actris.channel Require Import proofmode proto channel.
-From actris.logrel Require Import subtyping_rules term_typing_judgment term_typing_rules environments operators subtyping_rules.
-From iris.proofmode Require Import tactics.
+From actris.logrel Require Import subtyping_rules term_typing_rules.
+From actris.channel Require Import proofmode.
 
+(* FIXME
 Section mapper_example.
   Context `{heapG Σ, chanG Σ}.
 
@@ -16,31 +16,22 @@ Section mapper_example.
     lty_rec mapper_client_type_aux.
 
   Definition mapper_client : expr := λ: "c",
-    send "c" (λ: "x", #9000 < "x");; send "c" #42;; recv "c".
+    send "c" (λ: "x", #9000 < "x");;
+    send "c" #42;;
+    recv "c".
 
   Lemma mapper_client_typed Γ :
-    ⊢ Γ ⊨ mapper_client : (lty_chan (mapper_client_type) ⊸ lty_bool)%lty ⫤ Γ.
+    ⊢ Γ ⊨ mapper_client : lty_chan (mapper_client_type) ⊸ lty_bool.
   Proof.
-    iApply (ltyped_frame _ _ _ _ Γ).
-    { iApply env_split_id_l. }
-    2: { iApply env_split_id_l. }
-    iApply ltyped_lam.
-    { iApply env_split_id_r. }
-    iApply ltyped_let.
-    { iApply ltyped_send. apply lookup_insert.
-      iApply (ltyped_frame _ _ _ _ {["c":=_]}).
-      { iApply env_split_id_l. }
-      { iApply ltyped_lam.
-        { iApply env_split_id_r. }
-        iApply ltyped_bin_op.
-        - iApply ltyped_var. apply lookup_insert.
-        - iApply ltyped_int. }
-      { iApply env_split_id_l. } }
-    rewrite insert_insert /=.
-    iApply ltyped_let.
-    { iApply ltyped_send. apply lookup_insert.
-      iApply ltyped_int. }
-    rewrite insert_insert /=. iApply ltyped_recv. apply lookup_insert.
+    iApply (ltyped_frame _ [] []).
+    iApply (ltyped_lam []); simpl. iApply ltyped_weaken_post. iApply ltyped_let.
+    { iApply ltyped_send; last first.
+      { iApply (ltyped_lam []); simpl. iApply ltyped_weaken_post.
+        iApply ltyped_bin_op; [by iApply ltyped_var|]. by iApply ltyped_int. }
+      done. }
+    simpl. iApply ltyped_let.
+    { by iApply ltyped_send; [|by iApply ltyped_int]. }
+    simpl. by iApply ltyped_recv.
   Qed.
 
   (** Recursion and Swapping *)
@@ -62,9 +53,12 @@ Section mapper_example.
 
   Lemma mapper_client_rec_typed Γ :
     ⊢ Γ ⊨ mapper_client_rec :
-      (lty_chan (mapper_client_rec_type) ⊸ (lty_bool * lty_bool))%lty ⫤ Γ.
+          lty_chan (mapper_client_rec_type) ⊸ (lty_bool * lty_bool).
   Proof.
-    iApply (ltyped_frame _ _ _ _ Γ).
+    iApply (ltyped_frame _ [] []).
+    iApply (ltyped_lam []); simpl. iApply ltyped_weaken_post. iApply ltyped_let.
+
+
     { iApply env_split_id_l. }
     2: { iApply env_split_id_l. }
     iApply (ltyped_subsumption _ _ _((lty_chan (mapper_client_type_swap mapper_client_rec_type)) ⊸ _)).
@@ -261,3 +255,4 @@ Section mapper_example.
   Qed.
 
 End mapper_example.
+*)
diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
index 8d70e00727dd553ac23de67cd74ad2c785b1bae5..edaa305b7bde7e61c40d3d45073d310b66fce87b 100644
--- a/theories/logrel/examples/pair.v
+++ b/theories/logrel/examples/pair.v
@@ -7,22 +7,14 @@ can be assigned the type
   chan (?int.?int.end) ⊸ (int * int)
 
 by exclusively using the semantic typing rules. *)
-From actris.logrel Require Export environments term_typing_rules.
+From actris.logrel Require Export term_typing_rules.
 From iris.proofmode Require Import tactics.
 
 Definition prog : expr := λ: "c", (recv "c", recv "c").
 
-Section pair.
-  Context `{heapG Σ, chanG Σ}.
-
-  Lemma prog_typed :
-    ⊢ ∅ ⊨ prog : chan (<??> TY lty_int; <??> TY lty_int; END) ⊸ lty_int * lty_int.
-  Proof.
-    rewrite /prog.
-    iApply ltyped_lam.
-    { iApply env_split_id_r. }
-    iApply ltyped_pair. iApply ltyped_recv.
-    2:{ iApply ltyped_recv. by rewrite /binder_insert lookup_insert. }
-    by rewrite lookup_insert.
-  Qed.
-End pair.
+Lemma prog_typed `{heapG Σ, chanG Σ} :
+  ⊢ [] ⊨ prog : chan (<??> TY lty_int; <??> TY lty_int; END) ⊸ lty_int * lty_int.
+Proof.
+  iApply (ltyped_lam []); simpl. iApply ltyped_post_nil.
+  iApply ltyped_pair; [by iApply ltyped_recv|by iApply ltyped_recv].
+Qed.
diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
index 90445e66e42c24aaa1ea1b0b5cf2e1536b28cd6f..548959d4906971b60c4b2fc786aec4f0666d146d 100644
--- a/theories/logrel/lib/mutex.v
+++ b/theories/logrel/lib/mutex.v
@@ -40,12 +40,12 @@ Definition mutex_release : val :=
 (** Semantic types *)
 Definition lty_mutex `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ (γ : gname) (l : loc) (lk : val),
-    ⌜ w = PairV lk #l ⌝ ∗
+    ⌜ w = (lk,#l)%V ⌝ ∗
     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 ⌝ ∗
+    ⌜ w = (lk,#l)%V ⌝ ∗
     is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner) ∗
     spin_lock.locked γ ∗ l ↦ v)%I.
 
@@ -64,8 +64,7 @@ Section properties.
   Global Instance lty_mutex_ne : NonExpansive lty_mutex.
   Proof. solve_proper. Qed.
 
-  Global Instance lty_mutex_guard_contractive :
-    Contractive lty_mutex_guard.
+  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.
@@ -108,64 +107,47 @@ Section rules.
     ⊢ Γ ⊨ mutex_alloc : A → mutex A ⫤ Γ.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
-    iFrame "HΓ".
-    iIntros "!>" (v) "Hv". rewrite /mutex_alloc. wp_pures.
+    iIntros "{$HΓ} !>" (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=> //.
+    wp_pures. iExists γ, l, lk. eauto.
   Qed.
 
   Lemma ltyped_mutex_acquire Γ (x : string) A :
-    Γ !! x = Some (mutex A)%lty →
-    ⊢ Γ ⊨ mutex_acquire x : A ⫤ <[x := (mutex_guard A)%lty]> Γ.
+    env_filter_eq x Γ = [EnvItem x (mutex A)] →
+    ⊢ Γ ⊨ mutex_acquire x : A ⫤ env_cons x (mutex_guard A) Γ.
   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]".
+    iIntros (HΓx%env_filter_eq_perm' vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (env_ltyped_cons with "HΓ") as (vl Hvs) "[Hlock HΓ]"; rewrite Hvs.
+    iDestruct "Hlock" as (γ l lk ->) "#Hlock". rewrite /mutex_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Γ".
+    wp_load. iFrame "HA". iApply env_ltyped_cons.
+    iFrame "HΓ". iExists _; iSplit; [done|]. iExists γ, l, lk, v. auto with iFrame.
   Qed.
 
   Lemma ltyped_mutex_release Γ Γ' (x : string) e A :
-    Γ' !! x = Some (mutex_guard A)%lty →
+    env_filter_eq x Γ' = [EnvItem x (mutex_guard A)] →
     (Γ ⊨ e : A ⫤ Γ') -∗
-    Γ ⊨ mutex_release x e : () ⫤ <[x := (mutex A)%lty]> Γ'.
+    Γ ⊨ mutex_release x e : () ⫤ env_cons x (mutex A) Γ'.
   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.
+    iIntros (HΓx%env_filter_eq_perm') "#He". iIntros (vs) "!> HΓ /=".
+    wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HA HΓ']".
+    rewrite {2}HΓx /=.
+    iDestruct (env_ltyped_cons with "HΓ'") as (vl Hvs) "[Hguard HΓ']"; rewrite Hvs.
     iDestruct "Hguard" as (γ l lk inner ->) "(#Hlock & Hlocked & Hinner)".
-    rewrite /mutex_release.
-    wp_pures. wp_store. wp_pures.
+    rewrite /mutex_release. wp_store.
     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Γ'".
+      with "[$Hlock $Hlocked $Hinner]").
+    iIntros "_". iSplit; [done|].
+    iApply env_ltyped_cons. iFrame "HΓ'". iExists _; iSplit; [done|].
+    iExists γ, l, lk. auto.
   Qed.
-
 End rules.
diff --git a/theories/logrel/lib/par_start.v b/theories/logrel/lib/par_start.v
index ca7db424e212d5b7e5677d94adde8467fd53c1dc..9e9f40119af29f1ae4214191af4f4cfc8c3400cc 100644
--- a/theories/logrel/lib/par_start.v
+++ b/theories/logrel/lib/par_start.v
@@ -1,48 +1,23 @@
-From actris.logrel Require Export term_typing_rules environments.
+From actris.logrel Require Export term_typing_rules.
 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").
 
-  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.
+Lemma ltyped_par_start `{!heapG Σ, !chanG Σ, !spawnG Σ} Γ S A B :
+  ⊢ Γ ⊨ par_start : (chan S ⊸ A) ⊸ (chan (lty_dual S) ⊸ B) ⊸ A * B.
+Proof.
+  iApply (ltyped_lam []); iApply (ltyped_lam [EnvItem "e1" _] [] "e2"); simpl.
+  iApply ltyped_post_nil. iApply ltyped_let.
+  { iApply ltyped_app; [iApply ltyped_unit|iApply (ltyped_new_chan _ S)]. }
+  iApply ltyped_let; [by iApply ltyped_fst|]; simpl.
+  iApply ltyped_let; [by iApply ltyped_snd|]; simpl.
+  rewrite !(Permutation_swap (EnvItem "c1" _))
+    !(Permutation_swap (EnvItem "e1" _)).
+  iApply (ltyped_par [EnvItem "e1" _; EnvItem "c1" _]).
+  - iApply ltyped_app; by iApply ltyped_var.
+  - iApply ltyped_app; by iApply ltyped_var.
+Qed.
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 4df87806c451322ee0c0703c1a39a57acd0ae0f4..2d08421133fdbe17c967bbb50fb60c3db35e09d0 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -8,27 +8,47 @@ programs which satisfy the semantic typing relation are safe. That is,
 semantically well-typed programs do not get stuck. *)
 From iris.heap_lang Require Import metatheory adequacy.
 From actris.logrel Require Export term_types.
-From actris.logrel Require Import environments.
+From actris.logrel Require Export environments.
 From iris.proofmode Require Import tactics.
 
 (** The semantic typing judgment *)
 Definition ltyped `{!heapG Σ}
-    (Γ Γ' : gmap string (ltty Σ)) (e : expr) (A : ltty Σ) : iProp Σ :=
-  (■ ∀ vs, env_ltyped Γ vs -∗
-           WP subst_map vs e {{ v, ltty_car A v ∗ env_ltyped Γ' vs }})%I.
+    (Γ1 Γ2 : env Σ) (e : expr) (A : ltty Σ) : iProp Σ :=
+  tc_opaque (■ ∀ vs, env_ltyped vs Γ1 -∗
+    WP subst_map vs e {{ v, ltty_car A v ∗ env_ltyped vs Γ2 }})%I.
+Instance: Params (@ltyped) 2 := {}.
 
-Notation "Γ ⊨ e : A ⫤ Γ'" := (ltyped Γ Γ' e A)
+Notation "Γ1 ⊨ e : A ⫤ Γ2" := (ltyped Γ1 Γ2 e A)
   (at level 100, e at next level, A at level 200).
 Notation "Γ ⊨ e : A" := (Γ ⊨ e : A ⫤ Γ)
   (at level 100, e at next level, A at level 200).
 
+Section ltyped.
+  Context `{!heapG Σ}.
+
+  Global Instance ltyped_plain Γ1 Γ2 e A : Plain (ltyped Γ1 Γ2 e A).
+  Proof. rewrite /ltyped /=. apply _. Qed.
+  Global Instance ltyped_ne n :
+    Proper (dist n ==> dist n ==> (=) ==> dist n ==> dist n) (@ltyped Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance ltyped_proper :
+    Proper ((≡) ==> (≡) ==> (=) ==> (≡) ==> (≡)) (@ltyped Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance ltyped_Permutation :
+    Proper ((≡ₚ) ==> (≡ₚ) ==> (=) ==> (≡) ==> (≡)) (@ltyped Σ _).
+  Proof.
+    intros Γ1 Γ1' HΓ1 Γ2 Γ2' HΓ2 e ? <- A ? <-. rewrite /ltyped /=.
+    setoid_rewrite HΓ1. by setoid_rewrite HΓ2.
+  Qed.
+End ltyped.
+
 Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
-  (∀ `{heapG Σ}, ∃ A Γ', ⊢ ∅ ⊨ e : A ⫤ Γ') →
+  (∀ `{heapG Σ}, ∃ A, ⊢ [] ⊨ e : A ⫤ []) →
   rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
   is_Some (to_val e') ∨ reducible e' σ'.
 Proof.
   intros Hty. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?.
-  destruct (Hty _) as (A & Γ' & He). iIntros "_".
+  destruct (Hty _) as (A & He). iIntros "_".
   iDestruct (He $!∅ with "[]") as "He"; first by rewrite /env_ltyped.
   iEval (rewrite -(subst_map_empty e)). iApply (wp_wand with "He"); auto.
 Qed.
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index aa3328295911cbf5325f772177809cf45e286ddc..1a68f31c1fb15a3cac3e2dc2df35f86303217757 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -6,9 +6,7 @@ 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 Import environments.
+From actris.logrel Require Export subtyping_rules term_typing_judgment operators.
 From actris.utils Require Import switch.
 From actris.channel Require Import proofmode.
 
@@ -16,53 +14,54 @@ Section properties.
   Context `{heapG Σ}.
   Implicit Types A B : ltty Σ.
   Implicit Types S T : lsty Σ.
-  Implicit Types Γ : gmap string (ltty Σ).
+  Implicit Types Γ : env Σ.
 
   (** Frame rule *)
-  Lemma ltyped_frame Γ Γ' Γ1 Γ1' Γ2 e A :
-    env_split Γ Γ1 Γ2 -∗
-    (Γ1 ⊨ e : A ⫤ Γ1') -∗
-    env_split Γ' Γ1' Γ2 -∗
-    Γ ⊨ e : A ⫤ Γ'.
+  Lemma ltyped_frame Γ Γ1 Γ2 e A :
+    (Γ1 ⊨ e : A ⫤ Γ2) -∗
+    (Γ1 ++ Γ ⊨ e : A ⫤ Γ2 ++ Γ).
   Proof.
-    iIntros "#Hsplit #Htyped #Hsplit' !>" (vs) "Henv".
-    iDestruct ("Hsplit" with "Henv") as "[Henv1 Henv2]".
-    iApply (wp_wand with "(Htyped Henv1)").
-    iIntros (v) "[$ Henv1']".
-    iApply "Hsplit'". iFrame "Henv1' Henv2".
+    iIntros "#He !>" (vs) "HΓ".
+    iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 HΓ]".
+    iApply (wp_wand with "(He HΓ1)").
+    iIntros (v) "[$ HΓ2]". by iApply (env_ltyped_app with "[$]").
   Qed.
 
   (** Variable properties *)
   Lemma ltyped_var Γ (x : string) A :
-    Γ !! x = Some A → ⊢ Γ ⊨ x : A ⫤ <[x := (copy- A)%lty]> Γ.
+    env_filter_eq x Γ = [EnvItem x A] →
+    ⊢ Γ ⊨ x : A ⫤ env_cons x (copy- A) Γ.
   Proof.
-    iIntros (HΓx) "!>"; iIntros (vs) "HΓ /=".
-    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Γ".
+    iIntros (HΓx%env_filter_eq_perm') "!>"; iIntros (vs) "HΓ /=".
+    rewrite {1}HΓx /=.
+    iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]". rewrite Hvs.
+    iAssert (ltty_car (copy- A) v)%lty as "#HAm"; [by iApply coreP_intro|].
+    iApply wp_value. iFrame "HA". iApply env_ltyped_cons. eauto with iFrame.
   Qed.
 
   (** Subtyping *)
-  Theorem ltyped_subsumption Γ Γ2 e τ1 τ2 :
-    τ1 <: τ2 -∗ (Γ ⊨ e : τ1 ⫤ Γ2) -∗ (Γ ⊨ e : τ2 ⫤ Γ2).
+  Theorem ltyped_subsumption Γ1 Γ2 Γ1' Γ2' e τ τ' :
+    env_le Γ1 Γ1' -∗ τ' <: τ -∗ env_le Γ2' Γ2 -∗
+    (Γ1' ⊨ e : τ' ⫤ Γ2') -∗ (Γ1 ⊨ e : τ ⫤ Γ2).
+  Proof.
+    iIntros "#HleΓ1 #Hle #HleΓ2 #He" (vs) "!> HΓ1".
+    iApply (wp_wand with "(He (HleΓ1 HΓ1))").
+    iIntros (v) "[Hτ HΓ2]". iSplitL "Hτ"; [by iApply "Hle"|by iApply "HleΓ2"].
+  Qed.
+  Lemma ltyped_post_nil Γ1 Γ2 e τ :
+    (Γ1 ⊨ e : τ ⫤ Γ2) -∗ (Γ1 ⊨ e : τ ⫤ []).
   Proof.
-    iIntros "#Hle #Hltyped" (vs) "!> Henv".
-    iDestruct ("Hltyped" with "Henv") as "Hltyped'".
-    iApply (wp_wand with "Hltyped' [Hle]").
-    iIntros (v) "[H1 $]". by iApply "Hle".
+    iApply ltyped_subsumption;
+      [iApply env_le_refl|iApply lty_le_refl|iApply env_le_nil].
   Qed.
 
   (** Basic properties *)
   Lemma ltyped_unit Γ : ⊢ Γ ⊨ #() : ().
-  Proof. iIntros "!>" (vs) "HΓ /=". iApply wp_value. eauto. Qed.
+  Proof. iIntros "!>" (vs) "$ /=". iApply wp_value. eauto. Qed.
   Lemma ltyped_bool Γ (b : bool) : ⊢ Γ ⊨ #b : lty_bool.
-  Proof. iIntros "!>" (vs) "HΓ /=". iApply wp_value. eauto. Qed.
+  Proof. iIntros "!>" (vs) "$ /=". iApply wp_value. eauto. Qed.
   Lemma ltyped_int Γ (i : Z) : ⊢ Γ ⊨ #i : lty_int.
-  Proof. iIntros "!>" (vs) "HΓ /=". iApply wp_value. eauto. Qed.
+  Proof. iIntros "!>" (vs) "$ /=". iApply wp_value. eauto. Qed.
 
   (** Operations *)
   Lemma ltyped_un_op Γ1 Γ2 op e A B :
@@ -70,10 +69,9 @@ Section properties.
     (Γ1 ⊨ e : A ⫤ Γ2) -∗
     Γ1 ⊨ UnOp op e : B ⫤ Γ2.
   Proof.
-    iIntros (Hop) "#He !>". iIntros (vs) "HΓ1"=> /=.
-    wp_apply (wp_wand with "(He [HΓ1 //])"). iIntros (v1) "[HA HΓ2]".
-    iDestruct (Hop with "HA") as (w Heval) "HB".
-    wp_unop. iFrame.
+    iIntros (Hop) "#He !>". iIntros (vs) "HΓ1 /=".
+    wp_apply (wp_wand with "(He [HΓ1 //])"). iIntros (v1) "[HA $]".
+    iDestruct (Hop with "HA") as (w ?) "HB". by wp_unop.
   Qed.
 
   Lemma ltyped_bin_op Γ1 Γ2 Γ3 op e1 e2 A1 A2 B :
@@ -82,11 +80,10 @@ Section properties.
     (Γ2 ⊨ e1 : A1 ⫤ Γ3) -∗
     Γ1 ⊨ BinOp op e1 e2 : B ⫤ Γ3.
   Proof.
-    iIntros (Hop) "#He2 #He1 !>". iIntros (vs) "HΓ1"=> /=.
+    iIntros (Hop) "#He2 #He1 !>". iIntros (vs) "HΓ1 /=".
     wp_apply (wp_wand with "(He2 [HΓ1 //])"). iIntros (v2) "[HA2 HΓ2]".
-    wp_apply (wp_wand with "(He1 [HΓ2 //])"). iIntros (v1) "[HA1 HΓ3]".
-    iDestruct (Hop with "HA1 HA2") as (w Heval) "HB".
-    wp_binop. iFrame.
+    wp_apply (wp_wand with "(He1 [HΓ2 //])"). iIntros (v1) "[HA1 $]".
+    iDestruct (Hop with "HA1 HA2") as (w ?) "HB". by wp_binop.
   Qed.
 
   (** Conditionals *)
@@ -96,15 +93,13 @@ Section properties.
     (Γ2 ⊨ e3 : A ⫤ Γ3) -∗
     Γ1 ⊨ (if: e1 then e2 else e3) : A ⫤ Γ3.
   Proof.
-    iIntros "#He1 #He2 #He3 !>" (v) "HΓ1".
-    simpl.
+    iIntros "#He1 #He2 #He3 !>" (v) "HΓ1 /=".
     wp_apply (wp_wand with "(He1 [HΓ1 //])"). iIntros (b) "[Hbool HΓ2]".
     rewrite /lty_bool. iDestruct "Hbool" as ([]) "->".
-    - wp_apply (wp_wand with "(He2 [HΓ2 //])"). iIntros (w) "[HA HΓ3]". iFrame.
-    - wp_apply (wp_wand with "(He3 [HΓ2 //])"). iIntros (w) "[HA HΓ3]". iFrame.
+    - wp_apply (wp_wand with "(He2 [HΓ2 //])"). iIntros (w) "[$$]".
+    - wp_apply (wp_wand with "(He3 [HΓ2 //])"). iIntros (w) "[$$]".
   Qed.
 
-
   (** Arrow properties *)
   Lemma ltyped_app Γ1 Γ2 Γ3 e1 e2 A1 A2 :
     (Γ1 ⊨ e2 : A1 ⫤ Γ2) -∗ (Γ2 ⊨ e1 : A1 ⊸ A2 ⫤ Γ3) -∗
@@ -112,38 +107,35 @@ Section properties.
   Proof.
     iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
-    wp_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf HΓ]".
-    iApply wp_frame_r. iFrame "HΓ". iApply ("Hf" $! v with "HA1").
+    wp_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf $]".
+    iApply ("Hf" $! v with "HA1").
   Qed.
 
-  Lemma ltyped_lam Γ Γ1 Γ2 Γ' x e A1 A2 :
-    env_split Γ Γ1 Γ2 -∗
-    (<![x:=A1]!> Γ1 ⊨ e : A2 ⫤ Γ') -∗
-    Γ ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ Γ2.
+  Lemma ltyped_lam Γ1 Γ2 x e A1 A2 :
+    (env_cons x A1 Γ1 ⊨ e : A2 ⫤ []) -∗
+    Γ1 ++ Γ2 ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ env_filter_eq x Γ1 ++ Γ2.
   Proof.
-    iIntros "#Hsplit #He" (vs) "!> HΓ /=".
-    iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
-    wp_pures. iSplitL "HΓ1"; last done.
+    iIntros "#He" (vs) "!> HΓ /=". wp_pures.
+    rewrite {2}(env_filter_eq_perm Γ1 x) (comm _ (env_filter_eq x Γ1)) -assoc.
+    iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 $]".
     iIntros (v) "HA1". wp_pures.
-    iDestruct ("He" $!((binder_insert x v vs)) with "[HA1 HΓ1]") as "He'".
+    iDestruct ("He" $! (binder_insert x v vs) with "[HA1 HΓ1]") as "He'".
     { iApply (env_ltyped_insert with "[HA1 //] HΓ1"). }
-    iDestruct (wp_wand _ _ _ _ (ltty_car A2) with "He' []") as "He'".
-    { iIntros (w) "[$ _]". }
-    destruct x as [|x]; rewrite /= -?subst_map_insert //.
+    rewrite subst_map_binder_insert.
+    iApply (wp_wand with "He'"). by iIntros (w) "[$ _]".
   Qed.
 
   (* Typing rule for introducing copyable functions *)
-  Lemma ltyped_rec Γ Γ' Γ'' f x e A1 A2 :
-    env_copy Γ Γ' -∗
-    (<![f:=A1 → A2]!> $ <![x:=A1]!> Γ' ⊨ e : A2 ⫤ Γ'') -∗
-    Γ ⊨ (rec: f x := e) : A1 → A2 ⫤ ∅.
+  (* FIXME
+  Lemma ltyped_rec Γ1 Γ2 f x e A1 A2 :
+    (env_cons f (A1 → A2) (env_cons x A1 Γ1) ⊨ e : A2 ⫤ []) -∗
+    Γ1 ++ Γ2 ⊨ (rec: f x := e) : A1 → A2 ⫤ Γ2.
   Proof.
-    iIntros "#Hcopy #He". iIntros (vs) "!> HΓ /=". iApply wp_fupd. wp_pures.
-    iDestruct ("Hcopy" with "HΓ") as "HΓ".
-    iMod (fupd_mask_mono with "HΓ") as "#HΓ"; first done.
-    iModIntro. iSplitL; last by iApply env_ltyped_empty.
+    iIntros "#He". iIntros (vs) "!> HΓ /=". wp_pures.
+    iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 $]".
     iLöb as "IH".
     iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
+(*
     iDestruct ("He" $! (<![f:=r]!> $ <![x:=v]!> vs) with "[HΓ HA1]") as "He'".
     { iApply (env_ltyped_insert with "IH").
       iApply (env_ltyped_insert with "HA1 HΓ"). }
@@ -155,22 +147,23 @@ Section properties.
     - rewrite subst_subst_ne // -subst_map_insert.
       by rewrite -delete_insert_ne // -subst_map_insert.
   Qed.
+*)
+  Qed. *)
 
   Lemma ltyped_let Γ1 Γ2 Γ3 x e1 e2 A1 A2 :
-    (Γ1 ⊨ e1 : A1 ⫤ Γ2) -∗ (<![x:=A1]!> Γ2 ⊨ e2 : A2 ⫤ Γ3) -∗
-    Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ binder_delete x Γ3.
+    (Γ1 ⊨ e1 : A1 ⫤ Γ2) -∗
+    (env_cons x A1 Γ2 ⊨ e2 : A2 ⫤ Γ3) -∗
+    Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ env_filter_eq x Γ2 ++ env_filter_ne x Γ3.
   Proof.
-    iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1"=> /=.
-    wp_apply (wp_wand with "(He1 HΓ1)").
-    iIntros (v) "[HA1 HΓ2]".
-    wp_pures.
-    iDestruct (env_ltyped_insert _ _ x with "HA1 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 "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
+    wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HA1 HΓ2]". wp_pures.
+    rewrite {3}(env_filter_eq_perm Γ2 x).
+    iDestruct (env_ltyped_app with "HΓ2") as "[HΓ2eq HΓ2neq]".
+    iDestruct ("He2" $! (binder_insert x v vs) with "[HA1 HΓ2neq]") as "He'".
+    { by iApply (env_ltyped_insert with "HA1"). }
+    rewrite subst_map_binder_insert. iApply (wp_wand with "He'").
+    iIntros (w) "[$ HΓ3]".
+    iApply env_ltyped_app. iFrame "HΓ2eq". by iApply env_ltyped_delete.
   Qed.
 
   (** Product properties  *)
@@ -185,37 +178,27 @@ Section properties.
   Qed.
 
   Lemma ltyped_fst Γ A1 A2 (x : string) :
-    Γ !! x = Some (A1 * A2)%lty →
-    ⊢ Γ ⊨ Fst x : A1 ⫤ <[x := (copy- A1 * A2)%lty]> Γ.
+    env_filter_eq x Γ = [EnvItem x (A1 * A2)] →
+    ⊢ Γ ⊨ Fst x : A1 ⫤ env_cons x (copy- A1 * A2) Γ.
   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Γ".
+    iIntros (HΓx%env_filter_eq_perm' vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
+    iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures.
+    iAssert (ltty_car (copy- A1) v1)%lty as "#HA1m"; [by iApply coreP_intro|].
+    iFrame "HA1". iApply env_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ".
+    iExists v1, v2. eauto with iFrame.
   Qed.
 
   Lemma ltyped_snd Γ A1 A2 (x : string) :
-    Γ !! x = Some (A1 * A2)%lty →
-    ⊢ Γ ⊨ Snd x : A2 ⫤ <[x:=(A1 * copy- A2)%lty]> Γ.
+    env_filter_eq x Γ = [EnvItem x (A1 * A2)] →
+    ⊢ Γ ⊨ Snd x : A2 ⫤ env_cons x (A1 * copy- A2) Γ.
   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- 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Γ".
+    iIntros (HΓx%env_filter_eq_perm' vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
+    iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures.
+    iAssert (ltty_car (copy- A2) v2)%lty as "#HA2m"; [by iApply coreP_intro|].
+    iFrame "HA2". iApply env_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ".
+    iExists v1, v2. eauto with iFrame.
   Qed.
 
   (** Sum Properties *)
@@ -237,8 +220,6 @@ Section properties.
     iRight. iExists v. auto.
   Qed.
 
-  (* 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) -∗
@@ -246,29 +227,21 @@ Section properties.
     (Γ1 ⊨ Case e1 e2 e3 : B ⫤ Γ3).
   Proof.
     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".
+    wp_apply (wp_wand with "(H1 HΓ1)"). iIntros (s) "[[Hs|Hs] HΓ2]";
+      iDestruct "Hs" as (w ->) "HA"; wp_case.
+    - wp_apply (wp_wand with "(H2 HΓ2)"). iIntros (v) "[Hv $]".
+      iApply (wp_wand with "(Hv HA)"). auto.
+    - wp_apply (wp_wand with "(H3 HΓ2)"). iIntros (v) "[Hv $]".
+      iApply (wp_wand with "(Hv HA)"). auto.
   Qed.
 
   (** Universal Properties *)
-  Lemma ltyped_tlam Γ Γ1 Γ2 Γ' e k (C : lty Σ k → ltty Σ) :
-    env_split Γ Γ1 Γ2 -∗
-    (∀ M, Γ1 ⊨ e : C M ⫤ Γ') -∗
-    Γ ⊨ (λ: <>, e) : ∀ M, C M ⫤ Γ2.
+  Lemma ltyped_tlam Γ1 Γ2 Γ' e k (C : lty Σ k → ltty Σ) :
+    (∀ M, Γ1 ⊨ e : C M ⫤ []) -∗
+    Γ1 ++ Γ2 ⊨ (λ: <>, e) : ∀ M, C M ⫤ Γ2.
   Proof.
-    iIntros "#Hsplit #He" (vs) "!> HΓ /=". wp_pures.
-    iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
-    iSplitL "HΓ1"; last done.
+    iIntros "#He" (vs) "!> HΓ /=". wp_pures.
+    iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 $]".
     iIntros (M) "/=". wp_pures.
     iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[$ _]".
   Qed.
@@ -291,17 +264,19 @@ Section properties.
 
   Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 x e1 e2 (C : lty Σ k → ltty Σ) B :
     (Γ1 ⊨ e1 : ∃ M, C M ⫤ Γ2) -∗
-    (∀ Y, <![x:=C Y]!> Γ2 ⊨ e2 : B ⫤ Γ3) -∗
-    Γ1 ⊨ (let: x := e1 in e2) : B ⫤ binder_delete x Γ3.
+    (∀ Y, env_cons x (C Y) Γ2 ⊨ e2 : B ⫤ Γ3) -∗
+    Γ1 ⊨ (let: x := e1 in e2) : B ⫤ env_filter_eq x Γ2 ++ env_filter_ne x Γ3.
   Proof.
-    iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1"=> /=.
+    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) "[$ HΓ3]". by iApply env_ltyped_delete.
+    rewrite {3}(env_filter_eq_perm Γ2 x).
+    iDestruct (env_ltyped_app with "HΓ2") as "[HΓ2eq HΓ2neq]".
+    iDestruct ("He2" $! X (binder_insert x v vs) with "[HX HΓ2neq]") as "He'".
+    { by iApply (env_ltyped_insert with "HX"). }
+    rewrite subst_map_binder_insert. iApply (wp_wand with "He'").
+    iIntros (w) "[$ HΓ3]". iApply env_ltyped_app.
+    iFrame "HΓ2eq". by iApply env_ltyped_delete.
   Qed.
 
   (** Mutable Unique Reference properties *)
@@ -310,11 +285,8 @@ Section properties.
     (Γ1 ⊨ ref e : ref_uniq A ⫤ Γ2).
   Proof.
     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".
-    iFrame "HΓ2".
-    iExists l, v; iSplit=>//. iFrame "Hv Hl".
+    wp_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
+    wp_alloc l as "Hl". iExists l, v; eauto with iFrame.
   Qed.
 
   Lemma ltyped_free Γ1 Γ2 e A :
@@ -322,48 +294,34 @@ Section properties.
     (Γ1 ⊨ Free e : () ⫤ Γ2).
   Proof.
     iIntros "#He" (vs) "!> HΓ1 /=".
-    wp_bind (subst_map vs e).
-    iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv HΓ2]".
-    iDestruct "Hv" as (l w ->) "[Hl Hw]".
-    wp_free. by iFrame "HΓ2".
+    wp_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
+    iDestruct "Hv" as (l w ->) "[Hl Hw]". by wp_free.
   Qed.
 
   Lemma ltyped_load Γ (x : string) A :
-    Γ !! x = Some (ref_uniq A)%lty →
-    ⊢ Γ ⊨ ! x : A ⫤ <[x := (ref_uniq (copy- A))%lty]> Γ.
+    env_filter_eq x Γ = [EnvItem x (ref_uniq A)] →
+    ⊢ Γ ⊨ ! x : A ⫤ env_cons x (ref_uniq (copy- A)) Γ.
   Proof.
-    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_uniq (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Γ".
+    iIntros (HΓx%env_filter_eq_perm' vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
+    iDestruct "HA" as (l w ->) "[? HA]". wp_load.
+    iAssert (ltty_car (copy- A) w)%lty as "#HAm"; [by iApply coreP_intro|].
+    iFrame "HA". iApply env_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ".
+    iExists l, w. eauto with iFrame.
   Qed.
 
   Lemma ltyped_store Γ Γ' (x : string) e A B :
-    Γ' !! x = Some (ref_uniq A)%lty →
+    env_filter_eq x Γ' = [EnvItem x (ref_uniq A)] →
     (Γ ⊨ e : B ⫤ Γ') -∗
-    Γ ⊨ x <- e : () ⫤ <[x := (ref_uniq B)%lty]> Γ'.
+    Γ ⊨ x <- e : () ⫤ env_cons x (ref_uniq B) Γ'.
   Proof.
-    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_uniq 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Γ'".
+    iIntros (HΓx%env_filter_eq_perm') "#He"; iIntros (vs) "!> HΓ /=".
+    wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
+    rewrite {2}HΓx /=.
+    iDestruct (env_ltyped_cons with "HΓ'") as (vl Hvs) "[HA HΓ']"; rewrite Hvs.
+    iDestruct "HA" as (l w ->) "[? HA]". wp_store. iSplit; [done|].
+    iApply env_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ'".
+    iExists l, v. eauto with iFrame.
   Qed.
 
   (** Mutable Shared Reference properties *)
@@ -372,9 +330,8 @@ Section properties.
     Γ ⊨ e : ref_shr A ⫤ Γ'.
   Proof.
     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.
+    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv $]".
+    iDestruct "Hv" as (l w ->) "[Hl HA]". iExists l.
     iMod (inv_alloc (ref_shrN .@ l) _
       (∃ v : val, l ↦ v ∗ □ ltty_car A v) with "[Hl HA]") as "$"; last done.
     iExists w. iFrame "Hl HA".
@@ -385,14 +342,12 @@ Section properties.
     Γ ⊨ ! e : A ⫤ Γ'.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_bind (subst_map vs e).
-    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv HΓ]".
+    wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv $]".
     iDestruct "Hv" as (l ->) "#Hv".
     iInv (ref_shrN .@ l) as (v) "[>Hl #HA]" "Hclose".
     wp_load.
-    iMod ("Hclose" with "[Hl HA]") as "_".
-    { iExists v. iFrame "Hl HA". }
-    by iIntros "!> {$HΓ}".
+    iMod ("Hclose" with "[Hl HA]") as "_"; last done.
+    iExists v. iFrame "Hl HA".
   Qed.
 
   Lemma ltyped_store_shared Γ1 Γ2 Γ3 e1 e2 A :
@@ -401,16 +356,13 @@ Section properties.
     (Γ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_apply (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]".
+    iApply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw $]".
     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. by iSplit.
+    iMod ("Hclose" with "[Hl Hv]") as "_"; eauto.
   Qed.
 
   Lemma ltyped_fetch_and_add_shared Γ1 Γ2 Γ3 e1 e2 :
@@ -419,10 +371,8 @@ Section properties.
     (Γ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]".
+    wp_apply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
+    wp_apply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw $]".
     iDestruct "Hw" as (l ->) "#Hw".
     iInv (ref_shrN .@ l) as (w) "[Hl >Hn]" "Hclose".
     iDestruct "Hn" as %[k ->].
@@ -430,31 +380,22 @@ Section properties.
     wp_faa.
     iMod ("Hclose" with "[Hl]") as %_.
     { iExists #(k + n). iFrame "Hl". by iExists (k + n)%Z. }
-    iModIntro. iFrame "HΓ3". by iExists k.
+    by iExists k.
   Qed.
 
-  Section with_spawn.
-    Context `{spawnG Σ}.
-
-    (** Parallel composition properties *)
-    Lemma ltyped_par Γ Γ' Γ1 Γ1' Γ2 Γ2' e1 e2 A B :
-      env_split Γ Γ1 Γ2 -∗
-      (Γ1 ⊨ e1 : A ⫤ Γ1') -∗
-      (Γ2 ⊨ e2 : B ⫤ Γ2') -∗
-      env_split Γ' Γ1' Γ2' -∗
-      Γ ⊨ e1 ||| e2 : A * B ⫤ Γ'.
-    Proof.
-      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").
-      - 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.
+  (** Parallel composition properties *)
+  Lemma ltyped_par `{spawnG Σ} Γ1 Γ1' Γ2 Γ2' e1 e2 A B :
+    (Γ1 ⊨ e1 : A ⫤ Γ1') -∗
+    (Γ2 ⊨ e2 : B ⫤ Γ2') -∗
+    Γ1 ++ Γ2 ⊨ e1 ||| e2 : A * B ⫤ Γ1' ++ Γ2'.
+  Proof.
+    iIntros "#He1 #He2 !>" (vs) "HΓ /=".
+    iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 HΓ2]".
+    wp_apply (wp_par with "(He1 HΓ1) (He2 HΓ2)").
+    iIntros (v1 v2) "[[HA HΓ1'] [HB HΓ2']] !>". iSplitL "HA HB".
+    + iExists v1, v2. by iFrame.
+    + iApply env_ltyped_app. by iFrame.
+  Qed.
 
   (** Channel properties *)
   Section with_chan.
@@ -466,26 +407,22 @@ Section properties.
       iIntros (vs) "!> HΓ /=". iApply wp_value. iFrame "HΓ".
       iIntros (u) ">->".
       iApply (new_chan_spec with "[//]"); iIntros (c1 c2) "!> [Hp1 Hp2]".
-      iExists c1, c2. iSplit=>//. iFrame "Hp1 Hp2".
+      iExists c1, c2. by iFrame "Hp1 Hp2".
     Qed.
 
     Lemma ltyped_send Γ Γ' (x : string) e A S :
-      Γ' !! x = Some (chan (<!!> TY A; S))%lty →
+      env_filter_eq x Γ' = [EnvItem x (chan (<!!> TY A; S))] →
       (Γ ⊨ e : A ⫤ Γ') -∗
-      Γ ⊨ send x e : () ⫤ <[x:=(chan S)%lty]> Γ'.
+      Γ ⊨ send x e : () ⫤ env_cons x (chan S) Γ'.
     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 (v' Heq) "[Hc HΓ']".
-      { 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_id vs).
-    Qed.
+      iIntros (HΓx%env_filter_eq_perm') "#He !>". iIntros (vs) "HΓ /=".
+      wp_apply (wp_wand with "(He HΓ)"); iIntros (v) "[HA HΓ']".
+      rewrite {2}HΓx /=.
+      iDestruct (env_ltyped_cons with "HΓ'") as (c Hvs) "[Hc HΓ']". rewrite Hvs.
+      wp_send with "[HA //]". iSplitR; [done|].
+      iDestruct (env_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ'") as "HΓ' /=".
+      by rewrite  (insert_id vs).
+   Qed.
 
     Lemma iProto_le_lmsg_texist {kt : ktele Σ} (m : ltys Σ kt → iMsg Σ) :
       ⊢ (<?> (∃.. Xs : ltys Σ kt, m Xs)%lmsg) ⊑ (<? (Xs : ltys Σ kt)> m Xs).
@@ -496,61 +433,60 @@ Section properties.
       iApply (iProto_le_trans with "IH"). iIntros (Xs). by iExists (LTysS _ _).
     Qed.
 
-    Lemma ltyped_recv_texist {kt} Γ1 Γ2 M (xc : string) (x : binder) (e : expr)
+    Lemma ltyped_recv_texist {kt} Γ1 Γ2 M x (xc : string) (e : expr)
         (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) (B : ltty Σ) :
+      env_filter_eq xc Γ1 = [EnvItem xc (chan (<??> M))] →
       LtyMsgTele M A S →
       (∀ Ys,
-        <![x:=ktele_app A Ys]!> $ <[xc:=(chan (ktele_app S Ys))%lty]> Γ1 ⊨ e : B ⫤ Γ2) -∗
-      <[xc:=(chan (<??> M))%lty]> Γ1 ⊨
-        (let: x := recv xc in e) : B ⫤ binder_delete x Γ2.
+        env_cons x (ktele_app A Ys) (env_cons xc (chan (ktele_app S Ys)) Γ1) ⊨ e : B ⫤ Γ2) -∗
+      Γ1 ⊨ (let: x := recv xc in e) : B ⫤
+            env_filter_eq x (env_filter_ne xc Γ1) ++ env_filter_ne x Γ2.
     Proof.
       rewrite /LtyMsgTele.
-      iIntros (HM) "#He !>". iIntros (vs) "HΓ /=".
-      iDestruct (env_ltyped_lookup with "HΓ") as (c Hxc) "[Hc HΓ]".
-      { by apply lookup_insert. }
-      rewrite Hxc.
+      iIntros (HΓxc%env_filter_eq_perm' HM) "#He !>". iIntros (vs) "HΓ1 /=".
+      rewrite {2}HΓxc /=.
+      iDestruct (env_ltyped_cons with "HΓ1") as (c Hvs) "[Hc HΓ1]". rewrite Hvs.
+      rewrite {2}(env_filter_eq_perm (env_filter_ne xc Γ1) x).
+      iDestruct (env_ltyped_app with "HΓ1") as "[HΓ1eq HΓ1neq]".
       iAssert (c ↣ <? (Xs : ltys Σ kt) (v : val)>
-        MSG v {{ ltty_car (ktele_app A Xs) v }}; lsty_car (ktele_app S Xs)) with "[Hc]" as "Hc".
+        MSG v {{ ltty_car (ktele_app A Xs) v }};
+          lsty_car (ktele_app S Xs)) with "[Hc]" as "Hc".
       { iApply (iProto_mapsto_le with "Hc"); iIntros "!>". rewrite HM.
         iApply iProto_le_lmsg_texist. }
-      wp_recv (Xs v) as "HA". wp_pures.
-      rewrite -subst_map_binder_insert.
-      wp_apply (wp_wand with "(He [-]) []").
+      wp_recv (Xs v) as "HA". wp_pures. rewrite -subst_map_binder_insert.
+      wp_apply (wp_wand with "(He [- HΓ1eq])").
       { iApply (env_ltyped_insert _ _ x with "HA").
-        rewrite delete_insert_delete.
-        iEval (rewrite -(insert_id vs xc c) // -(insert_delete Γ1)).
-        by iApply (env_ltyped_insert _ _ xc with "[Hc] HΓ"). }
-      iIntros (w) "[$ HΓ]". by destruct x; [|by iApply env_ltyped_delete].
+        destruct (decide (x = xc)) as [->|].
+        - by rewrite env_filter_ne_cons.
+        - rewrite env_filter_ne_cons_ne //.
+          iApply env_ltyped_cons. eauto with iFrame. }
+      iIntros (w) "[$ HΓ]".
+      iApply env_ltyped_app. iFrame "HΓ1eq". by iApply env_ltyped_delete.
     Qed.
 
     Lemma ltyped_recv Γ (x : string) A S :
-      Γ !! x = Some (chan (<??> TY A; S))%lty →
-      ⊢ Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
+      env_filter_eq x Γ = [EnvItem x (chan (<??> TY A; S))] →
+      ⊢ Γ ⊨ recv x : A ⫤ env_cons x (chan S) Γ.
     Proof.
-      iIntros (Hx) "!>". iIntros (vs) "HΓ"=> /=.
-      iDestruct (env_ltyped_lookup _ _ _ _ (Hx) with "HΓ") as (v' Heq) "[Hc HΓ]".
-      rewrite Heq.
-      wp_recv (v) as "HA". iFrame "HA".
-      iDestruct (env_ltyped_insert _ _ x (chan _) _ with "[Hc //] HΓ") as "HΓ"=> /=.
-      by rewrite insert_delete (insert_id vs).
+      iIntros (HΓx%env_filter_eq_perm') "!>". iIntros (vs) "HΓ /=".
+      rewrite {1}HΓx /=.
+      iDestruct (env_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs.
+      wp_recv (v) as "HA". iFrame "HA". iApply env_ltyped_cons; eauto with iFrame.
     Qed.
 
     Definition select : val := λ: "c" "i", send "c" "i".
+
     Lemma ltyped_select Γ (x : string) (i : Z) (S : lsty Σ) Ss :
       Ss !! i = Some S →
-      ⊢ <[x:=(chan (lty_select Ss))%lty]>Γ ⊨ select x #i : () ⫤
-        <[x:=(chan S)%lty]>Γ.
+      env_filter_eq x Γ = [EnvItem x (chan (lty_select Ss))] →
+      ⊢ Γ ⊨ select x #i : () ⫤ env_cons x (chan S) Γ.
     Proof.
-      iIntros (Hin); iIntros "!>" (vs) "HΓ /=".
-      iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".
-      { by apply lookup_insert. }
-      rewrite Heq /select.
-      wp_send with "[]".
-      { eauto. }
-      iSplitR; first done.
+      iIntros (Hin HΓx%env_filter_eq_perm'); iIntros "!>" (vs) "HΓ /=".
+      rewrite {1}HΓx /=.
+      iDestruct (env_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs.
+      rewrite /select. wp_send with "[]"; [by eauto|]. iSplit; [done|].
       iDestruct (env_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ") as "HΓ' /=".
-      rewrite insert_delete insert_insert (insert_id vs)=> //.
-      by rewrite lookup_total_alt Hin.
+      by rewrite insert_id // lookup_total_alt Hin.
     Qed.
 
     Fixpoint lty_arr_list (As : list (ltty Σ)) (B : ltty Σ) : ltty Σ :=
@@ -600,23 +536,19 @@ Section properties.
     Lemma ltyped_branch Γ Ss A xs :
       (∀ x, x ∈ xs ↔ is_Some (Ss !! x)) →
       ⊢ Γ ⊨ branch xs : chan (lty_branch Ss) ⊸
-        lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A ⫤ ∅.
+        lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A ⫤ Γ.
     Proof.
-      iIntros (Hdom) "!>". iIntros (vs) "Hvs".
-      iApply wp_value.
-      iSplitL; last by iApply env_ltyped_empty.
+      iIntros (Hdom) "!>". iIntros (vs) "$". iApply wp_value.
       iIntros (c) "Hc". wp_lam.
       rewrite -subst_map_singleton.
-      iApply lty_arr_list_spec.
-      { by rewrite fmap_length. }
+      iApply lty_arr_list_spec; [by rewrite fmap_length|].
       iIntros (ws) "H".
       rewrite big_sepL2_fmap_l.
       iDestruct (big_sepL2_length with "H") as %Heq.
       rewrite -insert_union_singleton_r; last by apply lookup_map_string_seq_None.
       rewrite /= lookup_insert.
       wp_recv (x) as "HPsx". iDestruct "HPsx" as %HPs_Some.
-      wp_pures.
-      rewrite -subst_map_insert.
+      wp_pures. rewrite -subst_map_insert.
       assert (x ∈ xs) as Hin by naive_solver.
       pose proof (list_find_elem_of (x =.) xs x) as [[n z] Hfind_Some]; [done..|].
       iApply switch_body_spec.