From 13215e11b49b618115dfebfd49f0e61279f346df Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 22 Sep 2020 19:48:02 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20environment=20=E2=86=92=20context=20+?=
 =?UTF-8?q?=20some=20random=20cleanup=20along=20the=20way.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 README.md                                     |  11 +-
 _CoqProject                                   |   4 +-
 papers/CPP21.md                               |  13 +-
 theories/logrel/contexts.v                    | 243 ++++++++++++++++++
 theories/logrel/environments.v                | 243 ------------------
 theories/logrel/examples/choice_subtyping.v   |   3 +-
 .../logrel/examples/compute_client_list.v     |  45 ++--
 theories/logrel/examples/compute_service.v    |  23 +-
 theories/logrel/examples/mapper.v             |  26 +-
 theories/logrel/examples/mapper_list.v        | 119 ++++-----
 theories/logrel/examples/pair.v               |   2 +-
 theories/logrel/examples/par_recv.v           |  15 +-
 theories/logrel/examples/rec_subtyping.v      |   5 +-
 theories/logrel/lib/list.v                    |  11 +-
 theories/logrel/lib/mutex.v                   |  26 +-
 theories/logrel/lib/par_start.v               |  10 +-
 theories/logrel/session_typing_rules.v        |  48 ++--
 theories/logrel/term_typing_judgment.v        |  10 +-
 theories/logrel/term_typing_rules.v           | 119 +++++----
 19 files changed, 482 insertions(+), 494 deletions(-)
 create mode 100644 theories/logrel/contexts.v
 delete mode 100644 theories/logrel/environments.v

diff --git a/README.md b/README.md
index c4b618e..72903ee 100644
--- a/README.md
+++ b/README.md
@@ -140,9 +140,9 @@ The logical relation is defined across the following files:
   defined in [theories/logrel/model.v](theories/logrel/model.v).
 - [theories/logrel/operators.v](theories/logrel/operators.v):
   Type definitions of unary and binary operators.
-- [theories/logrel/environments.v](theories/logrel/environments.v):
-  Definition of the semantic type environment, which is used in the semantic
-  typing relation. This also contains the rules for updating the environment,
+- [theories/logrel/contexts.v](theories/logrel/contexts.v):
+  Definition of the semantic type contexts, which is used in the semantic
+  typing relation. This also contains the rules for updating the context,
   which is used for distributing affine resources across the
   various parts of the proofs inside the typing rules.
 - [theories/logrel/term_typing_judgment.v](theories/logrel/term_typing_judgment.v):
@@ -166,8 +166,9 @@ An extension to the basic type system is given in
 [theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), which defines
 mutexes as a type-safe abstraction. Mutexes are implemented using spin locks
 and allow one to gain exclusive ownership of resources shared between multiple
-threads.
-An encoding of a list type is found in [theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), along with auxillary lemmas, and a weakest precondition for `llength`,
+threads. An encoding of a list type is found in
+[theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), along with axillary
+lemmas, and a weakest precondition for `llength`,
 that converts ownership of a list type into a list reference predicate, with
 the values of the list made explicit.
 
diff --git a/_CoqProject b/_CoqProject
index 8e0851b..348e6fa 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -28,7 +28,7 @@ theories/examples/list_rev.v
 theories/logrel/model.v
 theories/logrel/telescopes.v
 theories/logrel/subtyping.v
-theories/logrel/environments.v
+theories/logrel/contexts.v
 theories/logrel/term_types.v
 theories/logrel/session_types.v
 theories/logrel/operators.v
@@ -47,4 +47,4 @@ theories/logrel/examples/choice_subtyping.v
 theories/logrel/examples/mapper.v
 theories/logrel/examples/mapper_list.v
 theories/logrel/examples/compute_service.v
-theories/logrel/examples/compute_client_list.v
\ No newline at end of file
+theories/logrel/examples/compute_client_list.v
diff --git a/papers/CPP21.md b/papers/CPP21.md
index 9c77769..93d4203 100644
--- a/papers/CPP21.md
+++ b/papers/CPP21.md
@@ -1,4 +1,4 @@
-## Differences
+# Differences between the paper and the mechanisation
 
 - The semantic encoding of ground types use existential quantification in the
   mechanization (e.g., `λ w. ∃ (x:Z), w = int`, while the paper uses set
@@ -14,16 +14,19 @@
 - The mechanisation employs a typing judgement for values (`ltyped_val`),
   for technical reasons. More details on this is found in
   [theories/logrel/term_typing_judgment.v](../theories/logrel/term_typing_judgment.v)
-## Examples
+
+# Examples
 
 - The parallel receive example in Section 4 can be found in
   [theories/logrel/examples/par_recv.v](../theories/logrel/examples/par_recv.v):
-  This program performs two ``racy'' parallel receives on the same channel from
+  This program performs two "racy" parallel receives on the same channel from
   two different threads, using locks to allow the channel to be shared.
 - The parallel compute client example in Section 4 can be found in
   [theories/logrel/examples/compute_client_list.v](../theories/logrel/examples/compute_client_list.v):
   This program sends computation requests and receives their results in parallel,
   analogous to the producer-consumer pattern. It uses a lock to share the channel
   and a shared counter, that keeps track of the number of computations in transit.
-  The computation service can be found in [theories/logrel/examples/compute_service.v](../theories/logrel/examples/compute_service.v). The definition of the list type
-  and the weakest precondition for `llength` can be found in [theories/logrel/lib/list.v](../theories/logrel/lib/list.v)
+  The computation service can be found in
+  [theories/logrel/examples/compute_service.v](../theories/logrel/examples/compute_service.v).
+  The definition of the list type and the weakest precondition for `llength`
+  can be found in [theories/logrel/lib/list.v](../theories/logrel/lib/list.v)
diff --git a/theories/logrel/contexts.v b/theories/logrel/contexts.v
new file mode 100644
index 0000000..2cc648a
--- /dev/null
+++ b/theories/logrel/contexts.v
@@ -0,0 +1,243 @@
+(** This file contains definitions related to type ctxironments. The following
+relations on ctxironments are defined:
+
+- [ctx_ltyped Γ vs]: This relation indicates that the value map [vs] contains a
+  value for each type in the semantic type ctxironment [Γ].
+- [ctx_split Γ Γ1 Γ2]: The semantic type ctxironment [Γ] can be split into
+  (semantically disjoint) [Γ1] and [Γ2].
+- [ctx_copy Γ Γ']: [Γ'] is a copyable sub-ctxironment of [Γ].
+
+In addition, some lemmas/rules about these definitions are proved, corresponding
+to the syntactic typing rules that are typically found in substructural type
+systems. *)
+From iris.algebra Require Export list.
+From iris.bi.lib Require Import core.
+From iris.proofmode Require Import tactics.
+From actris.logrel Require Export term_types subtyping_rules.
+
+Inductive ctx_item Σ := CtxItem {
+  ctx_item_name : string;
+  ctx_item_type : ltty Σ;
+}.
+Add Printing Constructor ctx_item.
+Arguments CtxItem {_} _ _.
+Arguments ctx_item_name {_} _.
+Arguments ctx_item_type {_} _.
+Instance: Params (@CtxItem) 2 := {}.
+Instance: Params (@ctx_item_type) 1 := {}.
+
+Section ctx_item_ofe.
+  Context {Σ : gFunctors}.
+  Instance ctx_item_equiv : Equiv (ctx_item Σ) := λ xA1 xA2,
+    ctx_item_name xA1 = ctx_item_name xA2 ∧ ctx_item_type xA1 ≡ ctx_item_type xA2.
+  Instance ctx_item_dist : Dist (ctx_item Σ) := λ n xA1 xA2,
+    ctx_item_name xA1 = ctx_item_name xA2 ∧ ctx_item_type xA1 ≡{n}≡ ctx_item_type xA2.
+  Lemma ctx_item_ofe_mixin : OfeMixin (ctx_item Σ).
+  Proof.
+    by apply (iso_ofe_mixin (A:=prodO (leibnizO string) (lttyO Σ))
+      (λ xA, (ctx_item_name xA, ctx_item_type xA))).
+  Qed.
+  Canonical Structure ctx_itemO := OfeT (ctx_item Σ) ctx_item_ofe_mixin.
+  Global Instance ctx_item_type_ne : NonExpansive (@ctx_item_type Σ).
+  Proof. by intros n ?? [??]. Qed.
+  Global Instance ctx_item_type_proper : Proper ((≡) ==> (≡)) (@ctx_item_type Σ).
+  Proof. by intros ?? [??]. Qed.
+End ctx_item_ofe.
+
+Notation ctx Σ := (list (ctx_item Σ)).
+
+Definition ctx_filter_eq {Σ} (x : binder) : ctx Σ → ctx Σ :=
+  filter (λ xA, x = BNamed (ctx_item_name xA)).
+Definition ctx_filter_ne {Σ} (x : binder) : ctx Σ → ctx Σ :=
+  filter (λ xA, x ≠ BNamed (ctx_item_name xA)).
+
+Arguments ctx_filter_eq _ !_ !_ / : simpl nomatch.
+Arguments ctx_filter_ne _ !_ !_ / : simpl nomatch.
+(** TODO: Move to std++, together with some lemmas about filter that can be
+factored out. *)
+Arguments filter _ _ _ _ _ !_ / : simpl nomatch.
+
+Instance ctx_lookup {Σ} : Lookup string (ltty Σ) (ctx Σ) := λ x Γ,
+  match ctx_filter_eq x Γ with
+  | [CtxItem _ A] => Some A
+  | _ => None
+  end.
+
+Definition ctx_cons {Σ} (b : binder) (A : ltty Σ) (Γ : ctx Σ) : ctx Σ :=
+  if b is BNamed x then CtxItem x A :: ctx_filter_ne x Γ else Γ.
+
+Definition ctx_ltyped {Σ} (vs : gmap string val) (Γ : ctx Σ) : iProp Σ :=
+  ([∗ list] iA ∈ Γ, ∃ v,
+    ⌜vs !! ctx_item_name iA = Some v⌝ ∗ ltty_car (ctx_item_type iA) v)%I.
+Instance: Params (@ctx_ltyped) 2 := {}.
+
+Definition ctx_le {Σ} (Γ1 Γ2 : ctx Σ) : iProp Σ :=
+  tc_opaque (■ ∀ vs, ctx_ltyped vs Γ1 -∗ ctx_ltyped vs Γ2)%I.
+Instance: Params (@ctx_le) 1 := {}.
+Infix "<ctx:" := ctx_le (at level 70) : bi_scope.
+Notation "Γ1 <ctx: Γ2" := (⊢ Γ1 <ctx: Γ2) (at level 70) : type_scope.
+
+Section ctx.
+  Context {Σ : gFunctors}.
+  Implicit Types A : ltty Σ.
+  Implicit Types Γ : ctx Σ.
+
+  (** ctx_filter *)
+  Lemma ctx_filter_eq_perm Γ x : Γ ≡ₚ ctx_filter_eq x Γ ++ ctx_filter_ne x Γ.
+  Proof.
+    rewrite /ctx_filter_eq /ctx_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 ctx_filter_ne_anon Γ : ctx_filter_ne BAnon Γ = Γ.
+  Proof. induction Γ as [|[y A] Γ IH]; by f_equal/=. Qed.
+
+  Lemma elem_of_ctx_filter_ne Γ x y B :
+    CtxItem y B ∈ ctx_filter_ne x Γ → x ≠ y.
+  Proof. intros ?%elem_of_list_filter. naive_solver. Qed.
+
+  Lemma ctx_filter_ne_cons Γ (x : string) A :
+    ctx_filter_ne x (CtxItem x A :: Γ) = ctx_filter_ne x Γ.
+  Proof. rewrite /ctx_filter_ne filter_cons_False; naive_solver. Qed.
+  Lemma ctx_filter_ne_cons_ne Γ x y A :
+    x ≠ BNamed y →
+    ctx_filter_ne x (CtxItem y A :: Γ) = CtxItem y A :: ctx_filter_ne x Γ.
+  Proof. intros. rewrite /ctx_filter_ne filter_cons_True; naive_solver. Qed.
+
+  Lemma ctx_lookup_perm Γ x A:
+    Γ !! x = Some A →
+    Γ ≡ₚ CtxItem x A :: ctx_filter_ne x Γ.
+  Proof.
+    rewrite /lookup /ctx_lookup=> ?.
+    destruct (ctx_filter_eq x Γ) as [|[x' ?] [|??]] eqn:Hx; simplify_eq/=.
+    assert (CtxItem x' A ∈ ctx_filter_eq x Γ)
+      as [? _]%elem_of_list_filter; simplify_eq/=.
+    { rewrite Hx. set_solver. }
+    by rewrite {1}(ctx_filter_eq_perm Γ x') Hx.
+  Qed.
+
+  (** ctx typing *)
+  Global Instance ctx_ltyped_Permutation vs :
+    Proper ((≡ₚ) ==> (⊣⊢)) (@ctx_ltyped Σ vs).	
+  Proof. intros Γ Γ' HΓ. by rewrite /ctx_ltyped HΓ. Qed.
+  Global Instance ctx_ltyped_ne vs : NonExpansive (@ctx_ltyped Σ vs).
+  Proof.
+    intros n Γ Γ' HΓ. rewrite /ctx_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 ctx_ltyped_proper vs : Proper ((≡) ==> (≡)) (@ctx_ltyped Σ vs).
+  Proof. apply (ne_proper _). Qed.
+
+  Lemma ctx_ltyped_nil vs : ⊢@{iPropI Σ} ctx_ltyped vs [].
+  Proof. done. Qed.
+
+  Lemma ctx_ltyped_app Γ1 Γ2 vs :
+    ctx_ltyped vs (Γ1 ++ Γ2) ⊣⊢ ctx_ltyped vs Γ1 ∗ ctx_ltyped vs Γ2.
+  Proof. apply big_opL_app. Qed.
+
+  Lemma ctx_ltyped_cons Γ vs x A : 
+    ctx_ltyped vs (CtxItem x A :: Γ) ⊣⊢ ∃ v,
+    ⌜vs !! x = Some v⌝ ∗ ltty_car A v ∗ ctx_ltyped vs Γ.
+  Proof.
+    iSplit; [by iIntros "[HA $]"|].
+    iDestruct 1 as (v ?) "[HA $]"; eauto.
+  Qed.
+
+  Lemma ctx_ltyped_insert Γ vs x A v :
+    ltty_car A v -∗
+    ctx_ltyped vs (ctx_filter_ne x Γ) -∗
+    ctx_ltyped (binder_insert x v vs) (ctx_cons x A Γ).
+  Proof.
+    iIntros "HA HΓ".
+    destruct x as [|x]; simpl; [rewrite ctx_filter_ne_anon; auto|].
+    iApply ctx_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_ctx_filter_ne).
+    iDestruct 1 as (w ?) "HB". iExists w. iIntros "{$HB} !%".
+    apply lookup_insert_Some; naive_solver.
+  Qed.
+
+  Lemma ctx_ltyped_insert' Γ vs x A v :
+    ltty_car A v -∗
+    ctx_ltyped vs Γ -∗
+    ctx_ltyped (binder_insert x v vs) (ctx_cons x A Γ).
+  Proof.
+    rewrite {1}(ctx_filter_eq_perm Γ x) ctx_ltyped_app.
+    iIntros "HA [_ HΓ]". by iApply (ctx_ltyped_insert with "HA").
+  Qed.
+
+  Lemma ctx_ltyped_delete Γ x v vs :
+    ctx_ltyped (binder_insert x v vs) Γ -∗
+    ctx_ltyped vs (ctx_filter_ne x Γ).
+  Proof.
+    rewrite {1}(ctx_filter_eq_perm Γ x) ctx_ltyped_app. iIntros "[_ HΓ]".
+    iApply (big_sepL_impl with "HΓ").
+    iIntros "!>" (k [j B] ?%elem_of_list_lookup_2%elem_of_ctx_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.
+
+  (** Ctxironment subtyping *)
+  Global Instance ctx_le_plain Γ1 Γ2 : Plain (Γ1 <ctx: Γ2).
+  Proof. rewrite /ctx_le /=. apply _. Qed.
+
+  Global Instance ctx_le_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡)) (@ctx_le Σ).
+  Proof.
+    intros Γ1 Γ1' HΓ1 Γ2 Γ2' HΓ2. rewrite /ctx_le /=.
+    setoid_rewrite HΓ1; by setoid_rewrite HΓ2.
+  Qed.
+  Global Instance ctx_le_ne : NonExpansive2 (@ctx_le Σ).
+  Proof. solve_proper. Qed.
+  Global Instance ctx_le_proper : Proper ((≡) ==> (≡) ==> (≡)) (@ctx_le Σ).
+  Proof. apply (ne_proper_2 _). Qed.
+
+  Lemma ctx_le_refl Γ : Γ <ctx: Γ.
+  Proof. iIntros (vs); auto. Qed.
+  Lemma ctx_le_trans Γ1 Γ2 Γ3 : Γ1 <ctx: Γ2 -∗ Γ2 <ctx: Γ3 -∗ Γ1 <ctx: Γ3.
+  Proof.
+    rewrite /ctx_le /=.
+    iIntros "#H1 #H2 !>" (vs) "Hvs". iApply "H2". by iApply "H1".
+  Qed.
+  Lemma ctx_le_nil Γ : Γ <ctx: [].
+  Proof. iIntros (vs) "!> _". iApply ctx_ltyped_nil. Qed.
+  Lemma ctx_le_cons x Γ1 Γ2 A1 A2 :
+    A1 <: A2 -∗ Γ1 <ctx: Γ2 -∗ CtxItem x A1 :: Γ1 <ctx: CtxItem x A2 :: Γ2.
+  Proof.
+    rewrite /ctx_le /=. iIntros "#H #H' !>" (vs) "Hvs".
+    iDestruct (ctx_ltyped_cons with "Hvs") as (v ?) "[Hv Hvs]".
+    iApply ctx_ltyped_cons. iExists _; iSplit; [done|].
+    iSplitL "Hv"; [by iApply "H"|by iApply "H'"].
+  Qed.
+  Lemma ctx_le_app Γ1 Γ2 Γ1' Γ2' :
+    Γ1 <ctx: Γ2 -∗ Γ1' <ctx: Γ2' -∗ Γ1 ++ Γ1' <ctx: Γ2 ++ Γ2'.
+  Proof.
+    rewrite /ctx_le /=. iIntros "#H #H' !>" (vs) "Hvs".
+    iDestruct (ctx_ltyped_app with "Hvs") as "[Hvs1 Hvs2]".
+    iApply ctx_ltyped_app. iSplitL "Hvs1"; [by iApply "H"|by iApply "H'"].
+  Qed.
+  Lemma ctx_le_copy x A :
+    [CtxItem x A] <ctx: [CtxItem x A; CtxItem x (copy- A)].
+  Proof.
+    iIntros "!>" (vs) "Hvs".
+    iDestruct (ctx_ltyped_cons with "Hvs") as (v ?) "[HA _]".
+    iAssert (ltty_car (copy- A) v)%lty as "#HAm"; [by iApply coreP_intro|].
+    iApply ctx_ltyped_cons. iExists _; iSplit; [done|]. iFrame "HA".
+    iApply ctx_ltyped_cons. iExists _; iSplit; [done|]. iFrame "HAm".
+    iApply ctx_ltyped_nil.
+  Qed.
+  Lemma ctx_le_copyable x A :
+    lty_copyable A -∗
+    [CtxItem x A] <ctx: [CtxItem x A; CtxItem x A].
+  Proof.
+    iIntros "#H". iApply ctx_le_trans; [iApply ctx_le_copy|].
+    iApply ctx_le_cons; [iApply lty_le_refl|].
+    iApply ctx_le_cons; [by iApply lty_le_copy_inv_elim_copyable|iApply ctx_le_nil].
+  Qed.
+End ctx.
diff --git a/theories/logrel/environments.v b/theories/logrel/environments.v
deleted file mode 100644
index a62fcaf..0000000
--- a/theories/logrel/environments.v
+++ /dev/null
@@ -1,243 +0,0 @@
-(** This file contains definitions related to type environments. The following
-relations on environments are defined:
-
-- [env_ltyped Γ vs]: This relation indicates that the value map [vs] contains a
-  value for each type in the semantic type environment [Γ].
-- [env_split Γ Γ1 Γ2]: The semantic type environment [Γ] can be split into
-  (semantically disjoint) [Γ1] and [Γ2].
-- [env_copy Γ Γ']: [Γ'] is a copyable sub-environment of [Γ].
-
-In addition, some lemmas/rules about these definitions are proved, corresponding
-to the syntactic typing rules that are typically found in substructural type
-systems. *)
-From iris.algebra Require Export list.
-From iris.bi.lib Require Import core.
-From actris.logrel Require Export term_types subtyping_rules.
-From iris.proofmode Require Import tactics.
-
-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.
-
-Instance env_lookup {Σ} : Lookup string (ltty Σ) (env Σ) := λ x Γ,
-  match env_filter_eq x Γ with
-  | [EnvItem _ A] => Some A
-  | _ => None
-  end.
-
-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 := {}.
-Infix "<env:" := env_le (at level 70) : bi_scope.
-Notation "Γ1 <env: Γ2" := (⊢ Γ1 <env: Γ2) (at level 70) : type_scope.
-
-Section env.
-  Context {Σ : gFunctors}.
-  Implicit Types A : ltty Σ.
-  Implicit Types Γ : env Σ.
-
-  (** env_filter *)
-  Lemma env_filter_eq_perm Γ x : Γ ≡ₚ env_filter_eq x Γ ++ env_filter_ne x Γ.
-  Proof.
-    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_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.
-
-  Lemma env_lookup_perm Γ x A:
-    Γ !! x = Some A →
-    Γ ≡ₚ EnvItem x A :: env_filter_ne x Γ.
-  Proof.
-    rewrite /lookup /env_lookup=> ?.
-    destruct (env_filter_eq x Γ) as [|[x' ?] [|??]] eqn:Hx; simplify_eq/=.
-    assert (EnvItem x' A ∈ env_filter_eq x Γ)
-      as [? _]%elem_of_list_filter; simplify_eq/=.
-    { rewrite Hx. set_solver. }
-    by rewrite {1}(env_filter_eq_perm Γ x') Hx.
-  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.
-    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_nil vs : ⊢@{iPropI Σ} env_ltyped vs [].
-  Proof. done. 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_ltyped_cons Γ vs x A : 
-    env_ltyped vs (EnvItem x A :: Γ) ⊣⊢ ∃ v,
-    ⌜vs !! x = Some v⌝ ∗ ltty_car A v ∗ env_ltyped vs Γ.
-  Proof.
-    iSplit; [by iIntros "[HA $]"|].
-    iDestruct 1 as (v ?) "[HA $]"; eauto.
-  Qed.
-
-  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 "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_ltyped_insert' Γ vs x A v :
-    ltty_car A v -∗
-    env_ltyped vs Γ -∗
-    env_ltyped (binder_insert x v vs) (env_cons x A Γ).
-  Proof.
-    rewrite {1}(env_filter_eq_perm Γ x) env_ltyped_app.
-    iIntros "HA [_ HΓ]". by iApply (env_ltyped_insert with "HA").
-  Qed.
-
-  Lemma env_ltyped_delete Γ x v vs :
-    env_ltyped (binder_insert x v vs) Γ -∗
-    env_ltyped vs (env_filter_ne x Γ).
-  Proof.
-    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.
-
-  (** Environment subtyping *)
-  Global Instance env_le_plain Γ1 Γ2 : Plain (Γ1 <env: Γ2).
-  Proof. rewrite /env_le /=. apply _. Qed.
-
-  Global Instance env_le_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡)) (@env_le Σ).
-  Proof.
-    intros Γ1 Γ1' HΓ1 Γ2 Γ2' HΓ2. rewrite /env_le /=.
-    setoid_rewrite HΓ1; by setoid_rewrite HΓ2.
-  Qed.
-  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: Γ.
-  Proof. iIntros (vs); auto. Qed.
-  Lemma env_le_trans Γ1 Γ2 Γ3 : Γ1 <env: Γ2 -∗ Γ2 <env: Γ3 -∗ Γ1 <env: Γ3.
-  Proof.
-    rewrite /env_le /=.
-    iIntros "#H1 #H2 !>" (vs) "Hvs". iApply "H2". by iApply "H1".
-  Qed.
-  Lemma env_le_nil Γ : Γ <env: [].
-  Proof. iIntros (vs) "!> _". iApply env_ltyped_nil. Qed.
-  Lemma env_le_cons x Γ1 Γ2 A1 A2 :
-    A1 <: A2 -∗ Γ1 <env: Γ2 -∗ EnvItem x A1 :: Γ1 <env: EnvItem x A2 :: Γ2.
-  Proof.
-    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_le_app Γ1 Γ2 Γ1' Γ2' :
-    Γ1 <env: Γ2 -∗ Γ1' <env: Γ2' -∗ Γ1 ++ Γ1' <env: Γ2 ++ Γ2'.
-  Proof.
-    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.
-  Lemma env_le_copy x A :
-    [EnvItem x A] <env: [EnvItem x A; EnvItem x (copy- A)].
-  Proof.
-    iIntros "!>" (vs) "Hvs".
-    iDestruct (env_ltyped_cons with "Hvs") as (v ?) "[HA _]".
-    iAssert (ltty_car (copy- A) v)%lty as "#HAm"; [by iApply coreP_intro|].
-    iApply env_ltyped_cons. iExists _; iSplit; [done|]. iFrame "HA".
-    iApply env_ltyped_cons. iExists _; iSplit; [done|]. iFrame "HAm".
-    iApply env_ltyped_nil.
-  Qed.
-  Lemma env_le_copyable x A :
-    lty_copyable A -∗
-    [EnvItem x A] <env: [EnvItem x A; EnvItem x A].
-  Proof.
-    iIntros "#H". iApply env_le_trans; [iApply env_le_copy|].
-    iApply env_le_cons; [iApply lty_le_refl|].
-    iApply env_le_cons; [by iApply lty_le_copy_inv_elim_copyable|iApply env_le_nil].
-  Qed.
-End env.
diff --git a/theories/logrel/examples/choice_subtyping.v b/theories/logrel/examples/choice_subtyping.v
index af3b01d..68d3fbe 100644
--- a/theories/logrel/examples/choice_subtyping.v
+++ b/theories/logrel/examples/choice_subtyping.v
@@ -4,9 +4,8 @@ example on page 23 of the paper:
 "On the Preciseness of Subtyping in Session Types"
 https://arxiv.org/pdf/1610.00328.pdf
 *)
-From actris.channel Require Import proofmode proto channel.
+From actris.channel Require Import proofmode.
 From actris.logrel Require Import subtyping_rules.
-From iris.proofmode Require Import tactics.
 
 Section choice_example.
   Context `{heapG Σ, chanG Σ}.
diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 9b41462..e24e07d 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -17,9 +17,8 @@ it is composed with the type checked service. *)
 From iris.algebra Require Import frac.
 From iris.heap_lang Require Import metatheory.
 From actris.utils Require Import llist.
-From actris.channel Require Import proofmode proto channel.
-From actris.logrel Require Import term_typing_rules session_typing_rules
-     subtyping_rules napp.
+From actris.channel Require Import proofmode.
+From actris.logrel Require Import session_typing_rules napp.
 From actris.logrel.lib Require Import list par_start.
 From actris.logrel.examples Require Import compute_service.
 
@@ -82,15 +81,15 @@ Section compute_example.
 
   Definition compute_type_invariant
              γ (A : ltty Σ) (c : val) (counter : loc) : iProp Σ :=
-    (∃ (n : nat) (b : bool),
-        (if b then True else own γ 1%Qp) ∗
-        counter ↦ #n ∗
-        c ↣ (lsty_car (lty_napp (recv_type A) n <++>
-               (if b then compute_type_client else END)%lty)))%I.
+    ∃ (n : nat) (b : bool),
+      (if b then True else own γ 1%Qp) ∗
+      counter ↦ #n ∗
+      c ↣ (lsty_car (lty_napp (recv_type A) n <++>
+             (if b then compute_type_client else END)%lty)).
 
   Lemma compute_type_client_unfold_app_cont A :
-    ⊢ compute_type_client <:
-        (cont_type A <++> (recv_type A <++> compute_type_client)).
+    compute_type_client <:
+      (cont_type A <++> (recv_type A <++> compute_type_client)).
   Proof.
     rewrite {1}/compute_type_client /lty_rec fixpoint_unfold.
     replace (fixpoint (compute_type_client_aux)) with
@@ -117,7 +116,7 @@ Section compute_example.
   Qed.
 
   Lemma compute_type_client_unfold_app_stop :
-    ⊢ compute_type_client <: lty_select (<[stop := END%lty]>∅).
+    compute_type_client <: lty_select (<[stop := END%lty]>∅).
   Proof.
     rewrite {1}/compute_type_client /lty_rec fixpoint_unfold.
     replace (fixpoint (compute_type_client_aux)) with
@@ -129,7 +128,7 @@ Section compute_example.
   Qed.
 
   Lemma recv_type_cont_type_swap A B :
-    ⊢ recv_type B <++> cont_type A <: cont_type A <++> recv_type B.
+    recv_type B <++> cont_type A <: cont_type A <++> recv_type B.
   Proof.
     iApply lty_le_trans.
     rewrite lty_app_recv lty_app_end_l.
@@ -145,7 +144,7 @@ Section compute_example.
   Qed.
 
   Lemma recv_type_stop_type_swap A :
-    ⊢ recv_type A <++> stop_type <: stop_type <++> recv_type A.
+    recv_type A <++> stop_type <: stop_type <++> recv_type A.
   Proof.
     iApply lty_le_trans.
     rewrite lty_app_recv lty_app_end_l.
@@ -269,17 +268,17 @@ Section compute_example.
   Qed.
 
   Lemma ltyped_compute_client Γ (A : ltty Σ) :
-    ⊢ Γ ⊨ compute_client : lty_list (() ⊸ A) ⊸
-                           chan compute_type_client ⊸
-                           lty_list A.
+    Γ ⊨ compute_client : lty_list (() ⊸ A) ⊸
+                         chan compute_type_client ⊸
+                         lty_list A.
   Proof.
     iApply ltyped_val_ltyped.
     iApply ltyped_val_lam.
     iApply ltyped_post_nil.
-    iApply (ltyped_lam [EnvItem "xs" _]).
+    iApply (ltyped_lam [CtxItem "xs" _]).
     iIntros "!>" (vs) "HΓ". simplify_map_eq.
-    iDestruct (env_ltyped_cons _ _ "c" with "HΓ") as (vc ->) "[Hc HΓ]".
-    iDestruct (env_ltyped_cons _ _ "xs" with "HΓ") as (vlxs ->) "[Hlxs HΓ]".
+    iDestruct (ctx_ltyped_cons _ _ "c" with "HΓ") as (vc ->) "[Hc HΓ]".
+    iDestruct (ctx_ltyped_cons _ _ "xs" with "HΓ") as (vlxs ->) "[Hlxs HΓ]".
     rewrite /lty_list /lty_rec fixpoint_unfold.
     iDestruct "Hlxs" as (l' v ->) "[Hlxs Hv]".
     wp_apply (llength_spec with "[Hlxs Hv]").
@@ -311,7 +310,7 @@ Section compute_example.
   Qed.
 
   Lemma lty_le_compute_type_dual :
-    ⊢ lty_dual compute_type_service <: compute_type_client.
+    lty_dual compute_type_service <: compute_type_client.
   Proof.
     rewrite /compute_type_client /compute_type_service.
     iLöb as "IH".
@@ -334,8 +333,8 @@ Section compute_example.
 
   Lemma ltyped_compute_list_par A e Γ Γ' :
     (Γ ⊨ e : lty_list (() ⊸ A) ⫤ Γ') -∗
-    Γ ⊨ par_start (compute_service) (compute_client e) :
-      (() * (lty_list A)) ⫤ Γ'.
+    (Γ ⊨ par_start (compute_service) (compute_client e) :
+       (() * (lty_list A)) ⫤ Γ').
   Proof.
     iIntros "He".
     iApply (ltyped_app with "[He]").
@@ -343,7 +342,7 @@ Section compute_example.
       iApply ltyped_compute_client. }
     iApply ltyped_app.
     { iApply ltyped_compute_service. }
-    iApply ltyped_subsumption; [ iApply env_le_refl | | iApply env_le_refl | ].
+    iApply ltyped_subsumption; [ iApply ctx_le_refl | | iApply ctx_le_refl | ].
     { iApply lty_le_arr; [ iApply lty_le_refl | ].
       iApply lty_le_arr; [ | iApply lty_le_refl ].
       iApply lty_le_arr; [ | iApply lty_le_refl ].
diff --git a/theories/logrel/examples/compute_service.v b/theories/logrel/examples/compute_service.v
index adcc7a6..79ac5fa 100644
--- a/theories/logrel/examples/compute_service.v
+++ b/theories/logrel/examples/compute_service.v
@@ -5,12 +5,9 @@
 
 It recursively receives computations, computes them, and then
 sends back the results. *)
-From iris.algebra Require Import frac.
 From iris.heap_lang Require Import metatheory.
-From actris.utils Require Import llist.
-From actris.channel Require Import proofmode proto channel.
-From actris.logrel Require Import term_typing_rules session_typing_rules
-     subtyping_rules napp.
+From actris.channel Require Import proofmode.
+From actris.logrel Require Import session_typing_rules.
 From actris.logrel.lib Require Import par_start.
 
 Definition cont : Z := 1.
@@ -37,11 +34,11 @@ Section compute_example.
 
   (** This judgement is checked only with the typing rules of the type system *)
   Lemma ltyped_compute_service Γ :
-    ⊢ Γ ⊨ compute_service : lty_chan compute_type_service ⊸ () ⫤ Γ.
+    Γ ⊨ compute_service : lty_chan compute_type_service ⊸ () ⫤ Γ.
   Proof.
     iApply (ltyped_subsumption _ _ _ _ _ _
               (lty_chan compute_type_service → ())%lty);
-      [ iApply env_le_refl | iApply lty_le_copy_elim | iApply env_le_refl | ].
+      [ iApply ctx_le_refl | iApply lty_le_copy_elim | iApply ctx_le_refl | ].
     iApply ltyped_val_ltyped.
     iApply ltyped_val_rec.
     iApply ltyped_post_nil.
@@ -51,7 +48,7 @@ Section compute_example.
               (chan (<?? A> TY () ⊸ A; <!!> TY A; compute_type_service) ⊸ ())%lty).
     {
       simpl.
-      iApply (ltyped_lam [EnvItem "go" _]).
+      iApply (ltyped_lam [CtxItem "go" _]).
       iApply ltyped_post_nil.
       iApply ltyped_recv_texist; [ done | apply _ | ].
       iIntros (Ys).
@@ -59,19 +56,19 @@ Section compute_example.
       pose proof (ltys_O_inv Ys') as HYs'.
       rewrite HYs HYs' /=.
       iApply ltyped_seq.
-      { iApply (ltyped_send _ [EnvItem "v" _; EnvItem "c" _; EnvItem "go" _]);
+      { iApply (ltyped_send _ [CtxItem "v" _; CtxItem "c" _; CtxItem "go" _]);
           [ done | ].
         iApply ltyped_app; [ by iApply ltyped_unit | ]=> /=.
         by iApply ltyped_var. }
       simpl.
       iApply ltyped_app; [ by iApply ltyped_var | ].
-      simpl. rewrite !(Permutation_swap (EnvItem "go" _)).
-      iApply ltyped_subsumption; [ | | iApply env_le_refl | ].
-      { iApply env_le_cons; [ iApply lty_le_refl | iApply env_le_nil ]. }
+      simpl. rewrite !(Permutation_swap (CtxItem "go" _)).
+      iApply ltyped_subsumption; [ | | iApply ctx_le_refl | ].
+      { iApply ctx_le_cons; [ iApply lty_le_refl | iApply ctx_le_nil ]. }
       { iApply lty_le_copy_elim. }
       by iApply ltyped_var. }
     iApply ltyped_app; [ by iApply ltyped_var | ].
-    iApply ltyped_subsumption; [ iApply env_le_nil | | iApply env_le_refl | ].
+    iApply ltyped_subsumption; [ iApply ctx_le_nil | | iApply ctx_le_refl | ].
     { iApply lty_le_arr; [ | iApply lty_le_refl ]. iApply lty_le_chan.
       iApply lty_le_l; [ iApply lty_le_rec_unfold | iApply lty_le_refl ]. }
     rewrite /compute_type_service_aux.
diff --git a/theories/logrel/examples/mapper.v b/theories/logrel/examples/mapper.v
index 4cf5514..55290e0 100644
--- a/theories/logrel/examples/mapper.v
+++ b/theories/logrel/examples/mapper.v
@@ -58,12 +58,12 @@ Section mapper_example.
     ("x","y").
 
   Lemma mapper_client_twice_typed Γ :
-    ⊢ Γ ⊨ mapper_client_twice :
+    Γ ⊨ mapper_client_twice :
           lty_chan (mapper_client_rec_type) ⊸ (lty_bool * lty_bool).
   Proof.
     iApply (ltyped_subsumption _ _ _ _ _ _
       ((lty_chan (mapper_client_type_swap mapper_client_rec_type)) ⊸ _)%lty);
-      [ iApply env_le_refl | | iApply env_le_refl | ].
+      [ iApply ctx_le_refl | | iApply ctx_le_refl | ].
     { iApply lty_le_arr; [ | iApply lty_le_refl ].
       iApply lty_le_chan.
       iApply lty_le_l; [ iApply lty_le_rec_unfold | ].
@@ -78,19 +78,19 @@ Section mapper_example.
       iApply lty_le_refl. }
     iApply (ltyped_lam []).
     iApply ltyped_seq.
-    { iApply (ltyped_send _ [EnvItem "c" _]); [ done | ].
+    { iApply (ltyped_send _ [CtxItem "c" _]); [ done | ].
       iApply (ltyped_lam []). iApply ltyped_post_nil.
       iApply ltyped_bin_op;
         [ by iApply ltyped_var | iApply ltyped_int ]. }
     iApply ltyped_seq.
-    { iApply (ltyped_send _ [EnvItem "c" _]); [ done | iApply ltyped_int ]. }
+    { iApply (ltyped_send _ [CtxItem "c" _]); [ done | iApply ltyped_int ]. }
     iApply ltyped_seq.
-    { iApply (ltyped_send _ [EnvItem "c" _]); [ done | ].
+    { iApply (ltyped_send _ [CtxItem "c" _]); [ done | ].
       iApply (ltyped_lam []). iApply ltyped_post_nil.
       iApply ltyped_bin_op;
         [ by iApply ltyped_var | iApply ltyped_int ]. }
     iApply ltyped_seq.
-    { iApply (ltyped_send _ [EnvItem "c" _]); [ done | iApply ltyped_int ]. }
+    { iApply (ltyped_send _ [CtxItem "c" _]); [ done | iApply ltyped_int ]. }
     iApply ltyped_post_nil.
     iApply ltyped_let; [ by iApply ltyped_recv | ].
     iApply ltyped_let; [ by iApply ltyped_recv | ].
@@ -120,13 +120,13 @@ Section mapper_example.
     ("x","y").
 
   Lemma mapper_client_twice_poly_typed Γ :
-    ⊢ Γ ⊨ mapper_client_twice_poly :
-      (lty_chan (mapper_client_rec_type_poly) ⊸ (lty_bool * lty_int))%lty ⫤ Γ.
+    Γ ⊨ mapper_client_twice_poly :
+      lty_chan (mapper_client_rec_type_poly) ⊸ (lty_bool * lty_int) ⫤ Γ.
   Proof.
     iApply (ltyped_subsumption _ _ _ _ _ _
       ((lty_chan (mapper_client_type_poly_swap mapper_client_rec_type_poly))
          ⊸ _)%lty);
-      [ iApply env_le_refl | | iApply env_le_refl | ].
+      [ iApply ctx_le_refl | | iApply ctx_le_refl | ].
     { iApply lty_le_arr; [ | iApply lty_le_refl ].
       iApply lty_le_chan.
       iApply lty_le_l; [ iApply lty_le_rec_unfold | ].
@@ -144,19 +144,19 @@ Section mapper_example.
       iApply lty_le_refl. }
     iApply (ltyped_lam []).
     iApply ltyped_seq.
-    { iApply (ltyped_send _ [EnvItem "c" _]); [ done | ].
+    { iApply (ltyped_send _ [CtxItem "c" _]); [ done | ].
       iApply (ltyped_lam []). iApply ltyped_post_nil.
       iApply ltyped_bin_op;
         [ by iApply ltyped_var | iApply ltyped_int ]. }
     iApply ltyped_seq.
-    { iApply (ltyped_send _ [EnvItem "c" _]); [ done | iApply ltyped_int ]. }
+    { iApply (ltyped_send _ [CtxItem "c" _]); [ done | iApply ltyped_int ]. }
     iApply ltyped_seq.
-    { iApply (ltyped_send _ [EnvItem "c" _]); [ done | ].
+    { iApply (ltyped_send _ [CtxItem "c" _]); [ done | ].
       iApply (ltyped_lam []). iApply ltyped_post_nil.
       iApply ltyped_if;
         [ iApply ltyped_bool | iApply ltyped_int | iApply ltyped_int ]. }
     iApply ltyped_seq.
-    { iApply (ltyped_send _ [EnvItem "c" _]); [ done | iApply ltyped_bool ]. }
+    { iApply (ltyped_send _ [CtxItem "c" _]); [ done | iApply ltyped_bool ]. }
     iApply ltyped_post_nil.
     iApply ltyped_let; [ by iApply ltyped_recv | ].
     iApply ltyped_let; [ by iApply ltyped_recv | ].
diff --git a/theories/logrel/examples/mapper_list.v b/theories/logrel/examples/mapper_list.v
index 5114621..2d114df 100644
--- a/theories/logrel/examples/mapper_list.v
+++ b/theories/logrel/examples/mapper_list.v
@@ -20,13 +20,10 @@ and have select and sends swapped ahead of the receives.
 An upfront version, where it using subtyping to unfold the recursive
 type an amount of types corresponding to the size of the list, after
 which all selects and seands are swapped ahead of all receives immediately. *)
-From actris.channel Require Import proofmode proto channel.
-From actris.logrel Require Import session_types subtyping_rules
-     term_typing_judgment term_typing_rules session_typing_rules
-     environments telescopes napp.
 From actris.utils Require Import llist.
+From actris.channel Require Import proofmode.
+From actris.logrel Require Import session_typing_rules napp.
 From actris.logrel.lib Require Import list par_start.
-From iris.proofmode Require Import tactics.
 
 Definition cont : Z := 1.
 Definition stop : Z := 2.
@@ -67,55 +64,53 @@ Definition mapper_prog : val :=
 Section mapper_example.
   Context `{heapG Σ, chanG Σ}.
 
-  Definition mapper_type_rec_service_aux (A : ltty Σ) (B : ltty Σ) (rec : lsty Σ)
-    : lsty Σ :=
+  Definition mapper_type_rec_service_aux (A B : ltty Σ) (rec : lsty Σ) : lsty Σ :=
     lty_branch $ <[cont := (<??> TY A; <!!> TY B ; rec)%lty]>
                $ <[stop := END%lty]> $ ∅.
-  Instance mapper_type_rec_service_contractive A B :
+  Instance mapper_type_rec_service_contractive (A B : ltty Σ) :
     Contractive (mapper_type_rec_service_aux A B).
   Proof. solve_proto_contractive. Qed.
-  Definition mapper_type_rec_service A B : lsty Σ :=
+  Definition mapper_type_rec_service (A B : ltty Σ) : lsty Σ :=
     lty_rec (mapper_type_rec_service_aux A B).
 
   Lemma ltyped_mapper_aux_service Γ A B :
-    ⊢ Γ ⊨ mapper_service_aux : (A → B) ⊸ lty_chan (mapper_type_rec_service A B) ⊸
+    Γ ⊨ mapper_service_aux : (A → B) ⊸ lty_chan (mapper_type_rec_service A B) ⊸
                                        () ⫤ Γ.
   Proof.
     iApply (ltyped_subsumption _ _ _ _ _ _
               ((A → B) → lty_chan (mapper_type_rec_service A B) ⊸ ())%lty);
-      [ iApply env_le_refl | iApply lty_le_copy_elim | iApply env_le_refl | ].
+      [ iApply ctx_le_refl | iApply lty_le_copy_elim | iApply ctx_le_refl | ].
     iApply ltyped_val_ltyped.
     iApply ltyped_val_rec.
-    iApply (ltyped_lam [EnvItem "go" _; EnvItem "f" _]).
+    iApply (ltyped_lam [CtxItem "go" _; CtxItem "f" _]).
     iApply ltyped_post_nil.
     iApply ltyped_app.
     { iApply (ltyped_lam []). iApply ltyped_post_nil. iApply ltyped_unit. }
     iApply ltyped_app.
-    {
-      simpl. rewrite !(Permutation_swap (EnvItem "f" _))
-                     !(Permutation_swap (EnvItem "go" _)).
-      iApply (ltyped_lam [EnvItem "go" _; EnvItem "f" _]).
+    { simpl. rewrite !(Permutation_swap (CtxItem "f" _))
+                     !(Permutation_swap (CtxItem "go" _)).
+      iApply (ltyped_lam [CtxItem "go" _; CtxItem "f" _]).
       iApply ltyped_post_nil.
       iApply ltyped_let; [ by iApply ltyped_recv | ].
       iApply ltyped_seq.
       { iApply (ltyped_send _
-                  [EnvItem "f" _; EnvItem "v" _; EnvItem "c" _; EnvItem "go" _]);
+                  [CtxItem "f" _; CtxItem "v" _; CtxItem "c" _; CtxItem "go" _]);
           [ done | ].
         iApply ltyped_app_copy; [ by iApply ltyped_var | ]=> /=.
-        rewrite !(Permutation_swap (EnvItem "f" _)).
+        rewrite !(Permutation_swap (CtxItem "f" _)).
         by iApply ltyped_var. }
-      simpl. rewrite !(Permutation_swap (EnvItem "f" _)).
-      iApply ltyped_subsumption; [ | iApply lty_le_refl | iApply env_le_refl | ].
-      { iApply env_le_cons; [ | iApply env_le_refl ].
+      simpl. rewrite !(Permutation_swap (CtxItem "f" _)).
+      iApply ltyped_subsumption; [ | iApply lty_le_refl | iApply ctx_le_refl | ].
+      { iApply ctx_le_cons; [ | iApply ctx_le_refl ].
         iApply lty_le_copy_inv_elim_copyable. iApply lty_copyable_arr_copy. }
       iApply ltyped_app; [ by iApply ltyped_var | ].
       iApply ltyped_app; [ by iApply ltyped_var | ].
-      simpl. rewrite !(Permutation_swap (EnvItem "go" _)).
-      iApply ltyped_subsumption; [ iApply env_le_refl | | iApply env_le_refl | ].
+      simpl. rewrite !(Permutation_swap (CtxItem "go" _)).
+      iApply ltyped_subsumption; [ iApply ctx_le_refl | | iApply ctx_le_refl | ].
       { iApply lty_le_copy_elim. }
       by iApply ltyped_var. }
     iApply ltyped_app; [ by iApply ltyped_var | ].
-    iApply ltyped_subsumption; [ iApply env_le_refl | | iApply env_le_refl | ].
+    iApply ltyped_subsumption; [ iApply ctx_le_refl | | iApply ctx_le_refl | ].
     { iApply lty_le_arr; [ | iApply lty_le_refl ]. iApply lty_le_chan.
       iApply lty_le_l; [ iApply lty_le_rec_unfold | iApply lty_le_refl ]. }
     iApply ltyped_branch. intros x. rewrite -elem_of_dom. set_solver.
@@ -125,7 +120,7 @@ Section mapper_example.
     <?? X Y> TY X → Y ; mapper_type_rec_service X Y.
 
   Lemma ltyped_mapper_service Γ :
-    ⊢ Γ ⊨ mapper_service : lty_chan (mapper_type_service) ⊸ () ⫤ Γ.
+    Γ ⊨ mapper_service : lty_chan (mapper_type_service) ⊸ () ⫤ Γ.
   Proof.
     iApply ltyped_val_ltyped.
     iApply ltyped_val_lam.
@@ -139,12 +134,12 @@ Section mapper_example.
     pose proof (ltys_O_inv Ks') as HKs'.
     rewrite HYs HKs HKs' /=.
     iApply (ltyped_subsumption _ []);
-      [ iApply env_le_nil | iApply lty_le_refl | iApply env_le_refl | ].
+      [ iApply ctx_le_nil | iApply lty_le_refl | iApply ctx_le_refl | ].
     iApply ltyped_mapper_aux_service.
   Qed.
 
   Definition mapper_type_rec_client_aux
-             (A : ltty Σ) (B : ltty Σ) (rec : lsty Σ) : lsty Σ :=
+             (A B : ltty Σ) (rec : lsty Σ) : lsty Σ :=
     lty_select $ <[cont := (<!!> TY A; <??> TY B ; rec)%lty]>
                $ <[stop := END%lty]> $ ∅.
   Instance mapper_type_rec_client_contractive A B :
@@ -164,10 +159,10 @@ Section mapper_example.
   Definition send_type (A : ltty Σ) : lsty Σ :=
     (lty_select (<[cont := <!!> TY A ; END ]>∅))%lty.
   Definition recv_type (B : ltty Σ) : lsty Σ :=
-    (<??> TY B ; END)%lty.
+    <??> TY B ; END.
 
   Lemma recv_type_send_type_swap A B :
-    ⊢ (recv_type B <++> send_type A <: send_type A <++> recv_type B)%lty.
+    recv_type B <++> send_type A <: send_type A <++> recv_type B.
   Proof.
     iApply lty_le_trans.
     rewrite lty_app_recv lty_app_end_l.
@@ -183,8 +178,8 @@ Section mapper_example.
   Qed.
 
   Lemma mapper_type_rec_client_unfold_app A B :
-    ⊢ mapper_type_rec_client A B <:
-        (send_type A <++> (recv_type B <++> mapper_type_rec_client A B))%lty.
+    mapper_type_rec_client A B <:
+      send_type A <++> (recv_type B <++> mapper_type_rec_client A B).
   Proof.
     rewrite {1}/mapper_type_rec_client /lty_rec fixpoint_unfold.
     replace (fixpoint (mapper_type_rec_client_aux A B)) with
@@ -203,9 +198,9 @@ Section mapper_example.
   Qed.
 
   Lemma mapper_type_rec_client_unfold_app_n A B n :
-    ⊢ mapper_type_rec_client A B <:
-         lty_napp (send_type A) n <++> (lty_napp (recv_type B) n <++>
-                                           mapper_type_rec_client A B).
+    mapper_type_rec_client A B <:
+       lty_napp (send_type A) n <++> (lty_napp (recv_type B) n <++>
+                                         mapper_type_rec_client A B).
   Proof.
     iInduction n as [|n] "IH"; simpl; [ | ].
     { rewrite /send_type /recv_type /=.
@@ -225,9 +220,9 @@ Section mapper_example.
   Qed.
 
   Lemma recv_mapper_type_rec_client_unfold_app A B n :
-    ⊢ (lty_napp (recv_type B) n <++> mapper_type_rec_client A B) <:
-      (send_type A <++>
-                 (lty_napp (recv_type B) (S n) <++> mapper_type_rec_client A B)).
+    lty_napp (recv_type B) n <++> mapper_type_rec_client A B <:
+    send_type A <++>
+               (lty_napp (recv_type B) (S n) <++> mapper_type_rec_client A B).
   Proof.
     iApply lty_le_trans.
     { iApply lty_le_app;
@@ -264,11 +259,11 @@ Section mapper_example.
 
   Lemma send_all_spec_aux A B c l xs n :
     {{{ llist (llist_type_pred A) l xs ∗
-        c ↣ lsty_car (lty_napp (recv_type B) n <++> (mapper_type_rec_client A B)) }}}
+        c ↣ lsty_car (lty_napp (recv_type B) n <++> mapper_type_rec_client A B) }}}
       send_all c #l
     {{{ RET #(); llist (llist_type_pred A) l [] ∗
                  c ↣ lsty_car (lty_napp (recv_type B) (length xs + n) <++>
-                                             (mapper_type_rec_client A B)) }}}.
+                                             mapper_type_rec_client A B) }}}.
   Proof.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH" forall (n).
@@ -294,7 +289,7 @@ Section mapper_example.
       send_all c #l
     {{{ RET #(); llist (llist_type_pred A) l [] ∗
                  c ↣ lsty_car (lty_napp (recv_type B) (length xs)
-                                             <++> (mapper_type_rec_client A B)) }}}.
+                                             <++> mapper_type_rec_client A B) }}}.
   Proof.
     iIntros (Φ) "[Hl Hc] HΦ".
     iApply (send_all_spec_aux _ _ _ _ _ 0 with "[$Hl Hc]").
@@ -325,22 +320,22 @@ Section mapper_example.
   Qed.
 
   Lemma ltyped_mapper_client_ad_hoc Γ (A B : ltty Σ) :
-    ⊢ Γ ⊨ mapper_client : (A → B) ⊸
-                          lty_list A ⊸
-                          chan mapper_type_client ⊸
-                          lty_list B.
+    Γ ⊨ mapper_client : (A → B) ⊸
+                        lty_list A ⊸
+                        chan mapper_type_client ⊸
+                        lty_list B.
   Proof.
     iApply ltyped_val_ltyped.
     iApply ltyped_val_lam.
-    iApply (ltyped_lam [EnvItem "f" _]).
-    iApply (ltyped_lam [EnvItem "xs" _; EnvItem "f" _]).
+    iApply (ltyped_lam [CtxItem "f" _]).
+    iApply (ltyped_lam [CtxItem "xs" _; CtxItem "f" _]).
     iIntros (vs) "!> HΓ /=".
     rewrite (lookup_delete_ne _ "n" "c")=> //.
     rewrite (lookup_delete_ne _ "n" "xs")=> //.
     rewrite lookup_delete=> //.
-    iDestruct (env_ltyped_cons _ _ "c" with "HΓ") as (vc ->) "[Hc HΓ]".
-    iDestruct (env_ltyped_cons _ _ "xs" with "HΓ") as (vl ->) "[Hl HΓ]".
-    iDestruct (env_ltyped_cons _ _ "f" with "HΓ") as (vf ->) "[Hf HΓ]".
+    iDestruct (ctx_ltyped_cons _ _ "c" with "HΓ") as (vc ->) "[Hc HΓ]".
+    iDestruct (ctx_ltyped_cons _ _ "xs" with "HΓ") as (vl ->) "[Hl HΓ]".
+    iDestruct (ctx_ltyped_cons _ _ "f" with "HΓ") as (vf ->) "[Hf HΓ]".
     wp_send with "[Hf//]".
     iDestruct (list_type_loc with "Hl") as %[l ->].
     wp_apply (llength_spec A with "Hl").
@@ -359,22 +354,22 @@ Section mapper_example.
   Qed.
 
   Lemma ltyped_mapper_client_upfront Γ (A B : ltty Σ) :
-    ⊢ Γ ⊨ mapper_client : (A → B) ⊸
-                          lty_list A ⊸
-                          chan mapper_type_client ⊸
-                          lty_list B.
+    Γ ⊨ mapper_client : (A → B) ⊸
+                        lty_list A ⊸
+                        chan mapper_type_client ⊸
+                        lty_list B.
   Proof.
     iApply ltyped_val_ltyped.
     iApply ltyped_val_lam.
-    iApply (ltyped_lam [EnvItem "f" _]).
-    iApply (ltyped_lam [EnvItem "xs" _; EnvItem "f" _]).
+    iApply (ltyped_lam [CtxItem "f" _]).
+    iApply (ltyped_lam [CtxItem "xs" _; CtxItem "f" _]).
     iIntros (vs) "!> HΓ /=".
     rewrite (lookup_delete_ne _ "n" "c")=> //.
     rewrite (lookup_delete_ne _ "n" "xs")=> //.
     rewrite (lookup_delete)=> //.
-    iDestruct (env_ltyped_cons _ _ "c" with "HΓ") as (vc ->) "[Hc HΓ]".
-    iDestruct (env_ltyped_cons _ _ "xs" with "HΓ") as (vl ->) "[Hl HΓ]".
-    iDestruct (env_ltyped_cons _ _ "f" with "HΓ") as (vf ->) "[Hf HΓ]".
+    iDestruct (ctx_ltyped_cons _ _ "c" with "HΓ") as (vc ->) "[Hc HΓ]".
+    iDestruct (ctx_ltyped_cons _ _ "xs" with "HΓ") as (vl ->) "[Hl HΓ]".
+    iDestruct (ctx_ltyped_cons _ _ "f" with "HΓ") as (vf ->) "[Hf HΓ]".
     wp_send with "[Hf//]".
     iDestruct (list_type_loc with "Hl") as %[l ->].
     wp_apply (llength_spec with "Hl").
@@ -395,7 +390,7 @@ Section mapper_example.
   Qed.
 
   Lemma lty_le_mapper_type_client_dual :
-    ⊢ lty_dual mapper_type_service <: mapper_type_client.
+    lty_dual mapper_type_service <: mapper_type_client.
   Proof.
     rewrite /mapper_type_client /mapper_type_service.
     iApply lty_le_l; [ iApply lty_le_dual_recv_exist | ]=> /=.
@@ -423,8 +418,8 @@ Section mapper_example.
     Lemma ltyped_mapper_prog A B e1 e2 Γ Γ' Γ'' :
       (Γ ⊨ e2 : lty_list A ⫤ Γ') -∗
       (Γ' ⊨ e1 : (A → B) ⫤ Γ'') -∗
-      Γ ⊨ par_start (mapper_service) (mapper_client e1 e2) :
-        (() * lty_list B) ⫤ Γ''.
+      (Γ ⊨ par_start (mapper_service) (mapper_client e1 e2) :
+        (() * lty_list B) ⫤ Γ'').
     Proof.
       iIntros "He2 He1".
       iApply (ltyped_app with "[He2 He1]").
@@ -434,7 +429,7 @@ Section mapper_example.
       iApply ltyped_app.
       { iApply ltyped_mapper_service. }
       iApply ltyped_subsumption;
-        [ iApply env_le_refl | | iApply env_le_refl | ].
+        [ iApply ctx_le_refl | | iApply ctx_le_refl | ].
       { iApply lty_le_arr; [ iApply lty_le_refl | ].
         iApply lty_le_arr; [ | iApply lty_le_refl ].
         iApply lty_le_arr; [ | iApply lty_le_refl ].
diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
index 975d5e4..34228f1 100644
--- a/theories/logrel/examples/pair.v
+++ b/theories/logrel/examples/pair.v
@@ -13,7 +13,7 @@ From iris.proofmode Require Import tactics.
 Definition prog : expr := λ: "c", (recv "c", recv "c").
 
 Lemma prog_typed `{heapG Σ, chanG Σ} :
-  ⊢ [] ⊨ 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.
   iApply (ltyped_lam []); simpl. iApply ltyped_post_nil.
   iApply ltyped_pair; [by iApply ltyped_recv|by iApply ltyped_recv].
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index 950cf64..6d55ddf 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -17,7 +17,6 @@ From iris.algebra Require Import frac auth excl updates.
 From iris.heap_lang.lib Require Export par spin_lock.
 From actris.channel Require Import proofmode.
 From actris.logrel Require Export term_typing_judgment session_types.
-From actris.logrel Require Import environments.
 
 Definition prog : val := λ: "c",
   let: "lock" := newlock #() in
@@ -41,9 +40,9 @@ Section double.
     (<? (x : Z)> MSG #x; <? (y : Z)> MSG #y; END)%proto.
 
   Definition chan_inv (c : val) (γ : gname) : iProp Σ :=
-    (c ↣ prog_prot ∨
+    c ↣ prog_prot ∨
      (own γ (1/2)%Qp ∗ c ↣ <? (x : Z)> MSG #x; END) ∨
-     (own γ 1%Qp ∗ c ↣ END))%I.
+     (own γ 1%Qp ∗ c ↣ END).
 
   Lemma wp_prog c :
     {{{ ▷ c ↣ prog_prot }}}
@@ -101,7 +100,7 @@ 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.
@@ -126,13 +125,13 @@ Section double_fc.
 
   Definition chan_inv_fc (γ γ1 γ2 : gname) (P : val → val → iProp Σ) (c : val) :
     iProp Σ :=
-    (own γ (Excl ()) ∗ c ↣ prog_prot_fc P ∨
+    own γ (Excl ()) ∗ c ↣ prog_prot_fc P ∨
      (∃ b v1,
        own (if b : bool then γ1 else γ2) (3/4, to_agree (Some v1))%Qp ∗
        c ↣ <? (v2 : val)> MSG v2 {{ P v1 v2 }}; END) ∨
      (∃ v1 v2,
        own γ1 (1/4, to_agree (Some v1))%Qp ∗
-       own γ2 (1/4, to_agree (Some v2))%Qp))%I.
+       own γ2 (1/4, to_agree (Some v2))%Qp).
 
   Lemma wp_prog_fc P c :
     {{{ ▷ c ↣ prog_prot_fc P }}}
@@ -212,10 +211,10 @@ Section double_fc.
   Qed.
 
   Lemma prog_typed_fc :
-    ⊢ [] ⊨ 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_nil.
+    iApply wp_value. iSplitL; last by iApply ctx_ltyped_nil.
     iIntros (c) "Hc".
     iApply (wp_prog_fc (λ 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/rec_subtyping.v b/theories/logrel/examples/rec_subtyping.v
index a8f277e..e1abf8a 100644
--- a/theories/logrel/examples/rec_subtyping.v
+++ b/theories/logrel/examples/rec_subtyping.v
@@ -5,9 +5,8 @@ In pseudo syntax, the subtyping we show is:
      μ rec. ! (X,Y:★) (X ⊸ Y). !X. ?Y. rec
   <: μ rec. ! (X1,X2:★) (X1 ⊸ bool). !X1. !(X2 ⊸ int). !X2. ?bool. ?int. rec
 *)
-From actris.channel Require Import proofmode proto channel.
+From actris.channel Require Import proofmode.
 From actris.logrel Require Import subtyping_rules.
-From iris.proofmode Require Import tactics.
 
 Section basics.
   Context `{heapG Σ, chanG Σ}.
@@ -33,7 +32,7 @@ Section basics.
   Proof. solve_proto_contractive. Qed.
   Definition prot2 := lty_rec prot2_aux.
 
-  Lemma rec_swap_example : ⊢ prot1 <: prot2.
+  Lemma rec_swap_example : prot1 <: prot2.
   Proof.
     iApply (lty_le_trans _ prot1').
     { iLöb as "IH".
diff --git a/theories/logrel/lib/list.v b/theories/logrel/lib/list.v
index e33563a..6f14340 100644
--- a/theories/logrel/lib/list.v
+++ b/theories/logrel/lib/list.v
@@ -25,8 +25,7 @@ Section with_Σ.
     (λ v w : val, ⌜v = w⌝ ∗ ltty_car A v)%I.
 
   Lemma llist_lty_list lys ys A :
-    llist (llist_type_pred A) lys ys -∗
-          ltty_car (lty_list A) #lys.
+    llist (llist_type_pred A) lys ys -∗ ltty_car (lty_list A) #lys.
   Proof.
     iIntros "Hlys".
     iInduction ys as [|y ys] "IH" forall (lys).
@@ -44,11 +43,11 @@ Section with_Σ.
   Qed.
 
   Lemma llength_spec A (l : loc) :
-    ⊢ {{{ ltty_car (list A) #l }}} llength #l
-      {{{ xs (n:Z), RET #n; ⌜Z.of_nat (length xs) = n⌝ ∗
-                            llist (llist_type_pred A) l xs }}}.
+    {{{ ltty_car (list A) #l }}} llength #l
+    {{{ xs (n:Z), RET #n; ⌜Z.of_nat (length xs) = n⌝ ∗
+                          llist (llist_type_pred A) l xs }}}.
   Proof.
-    iIntros "!>" (Φ) "Hl HΦ".
+    iIntros (Φ) "Hl HΦ".
     iLöb as "IH" forall (l Φ).
     wp_lam.
     rewrite {2}/lty_list /lty_rec /lty_list_aux fixpoint_unfold.
diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
index ed39324..839c7b0 100644
--- a/theories/logrel/lib/mutex.v
+++ b/theories/logrel/lib/mutex.v
@@ -24,12 +24,10 @@ This type former is strongly inspired by the [Mutex] type in the standard
 library of Rust, which has also been semantically modelled in the LambdaRust
 project.
 *)
-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.lib Require Export spin_lock.
 From iris.heap_lang Require Import metatheory.
+From actris.channel Require Import proofmode.
+From actris.logrel Require Export term_types term_typing_judgment subtyping.
 
 (** Mutex functions *)
 Definition mutex_alloc : val := λ: "x", (newlock #(), ref "x").
@@ -104,7 +102,7 @@ Section rules.
 
   (** Mutex properties *)
   Lemma ltyped_mutex_alloc Γ A :
-    ⊢ Γ ⊨ mutex_alloc : A → mutex A ⫤ Γ.
+    Γ ⊨ mutex_alloc : A → mutex A ⫤ Γ.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
     iIntros "{$HΓ} !>" (v) "Hv". rewrite /mutex_alloc. wp_pures.
@@ -119,26 +117,26 @@ Section rules.
 
   Lemma ltyped_mutex_acquire Γ (x : string) A :
     Γ !! x = Some (mutex A)%lty →
-    ⊢ Γ ⊨ mutex_acquire x : A ⫤ env_cons x (mutex_guard A) Γ.
+    Γ ⊨ mutex_acquire x : A ⫤ ctx_cons x (mutex_guard A) Γ.
   Proof.
-    iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
-    iDestruct (env_ltyped_cons with "HΓ") as (vl Hvs) "[Hlock HΓ]"; rewrite Hvs.
+    iIntros (HΓx%ctx_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (ctx_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_load. iFrame "HA". iApply env_ltyped_cons.
+    wp_load. iFrame "HA". iApply ctx_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 →
     (Γ ⊨ e : A ⫤ Γ') -∗
-    Γ ⊨ mutex_release x e : () ⫤ env_cons x (mutex A) Γ'.
+    (Γ ⊨ mutex_release x e : () ⫤ ctx_cons x (mutex A) Γ').
   Proof.
-    iIntros (HΓx%env_lookup_perm) "#He". iIntros (vs) "!> HΓ /=".
+    iIntros (HΓx%ctx_lookup_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 (ctx_ltyped_cons with "HΓ'") as (vl Hvs) "[Hguard HΓ']"; rewrite Hvs.
     iDestruct "Hguard" as (γ l lk inner ->) "(#Hlock & Hlocked & Hinner)".
     rewrite /mutex_release. wp_store.
     iAssert (∃ inner, l ↦ inner ∗ ltty_car A inner)%I
@@ -147,7 +145,7 @@ Section rules.
     wp_apply (release_spec γ _ (∃ inner, l ↦ inner ∗ ltty_car A inner)%I
       with "[$Hlock $Hlocked $Hinner]").
     iIntros "_". iSplit; [done|].
-    iApply env_ltyped_cons. iFrame "HΓ'". iExists _; iSplit; [done|].
+    iApply ctx_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 acf843c..5f0e2e2 100644
--- a/theories/logrel/lib/par_start.v
+++ b/theories/logrel/lib/par_start.v
@@ -10,16 +10,16 @@ Definition par_start : expr := λ: "e1" "e2",
   ("e1" "c1") ||| ("e2" "c2").
 
 Lemma ltyped_par_start `{!heapG Σ, !chanG Σ, !spawnG Σ} Γ S A B :
-  ⊢ Γ ⊨ par_start : (chan S ⊸ A) ⊸ (chan (lty_dual S) ⊸ B) ⊸ 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_lam []); iApply (ltyped_lam [CtxItem "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" _]).
+  rewrite !(Permutation_swap (CtxItem "c1" _))
+    !(Permutation_swap (CtxItem "e1" _)).
+  iApply (ltyped_par [CtxItem "e1" _; CtxItem "c1" _]).
   - iApply ltyped_app; by iApply ltyped_var.
   - iApply ltyped_app; by iApply ltyped_var.
 Qed.
diff --git a/theories/logrel/session_typing_rules.v b/theories/logrel/session_typing_rules.v
index ee94896..e94d0c8 100644
--- a/theories/logrel/session_typing_rules.v
+++ b/theories/logrel/session_typing_rules.v
@@ -13,7 +13,7 @@ Section session_typing_rules.
   Context `{!heapG Σ, !chanG Σ}.
   Implicit Types A B : ltty Σ.
   Implicit Types S T : lsty Σ.
-  Implicit Types Γ : env Σ.
+  Implicit Types Γ : ctx Σ.
 
   Lemma ltyped_new_chan Γ S :
     Γ ⊨ new_chan : () ⊸ (chan S * chan (lty_dual S)) ⫤ Γ.
@@ -27,14 +27,14 @@ Section session_typing_rules.
   Lemma ltyped_send Γ Γ' (x : string) e A S :
     Γ' !! x = Some (chan (<!!> TY A; S))%lty →
     (Γ ⊨ e : A ⫤ Γ') -∗
-    (Γ ⊨ send x e : () ⫤ env_cons x (chan S) Γ').
+    (Γ ⊨ send x e : () ⫤ ctx_cons x (chan S) Γ').
   Proof.
-    iIntros (HΓx%env_lookup_perm) "#He !>". iIntros (vs) "HΓ /=".
+    iIntros (HΓx%ctx_lookup_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.
+    iDestruct (ctx_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Γ' /=".
+    iDestruct (ctx_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ'") as "HΓ' /=".
     by rewrite  (insert_id vs).
  Qed.
 
@@ -52,16 +52,16 @@ Section session_typing_rules.
     Γ1 !! xc = Some (chan (<??> M))%lty →
     LtyMsgTele M A S →
     (∀ Ys,
-      env_cons x (ktele_app A Ys) (env_cons xc (chan (ktele_app S Ys)) Γ1) ⊨ e : B ⫤ Γ2) -∗
+      ctx_cons x (ktele_app A Ys) (ctx_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.
+          ctx_filter_eq x (ctx_filter_ne xc Γ1) ++ ctx_filter_ne x Γ2.
   Proof.
     rewrite /LtyMsgTele.
-    iIntros (HΓxc%env_lookup_perm HM) "#He !>". iIntros (vs) "HΓ1 /=".
+    iIntros (HΓxc%ctx_lookup_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]".
+    iDestruct (ctx_ltyped_cons with "HΓ1") as (c Hvs) "[Hc HΓ1]". rewrite Hvs.
+    rewrite {2}(ctx_filter_eq_perm (ctx_filter_ne xc Γ1) x).
+    iDestruct (ctx_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".
@@ -69,23 +69,23 @@ Section session_typing_rules.
       iApply iProto_le_lmsg_texist. }
     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").
+    { iApply (ctx_ltyped_insert _ _ x with "HA").
       destruct (decide (x = xc)) as [->|].
-      - by rewrite env_filter_ne_cons.
-      - rewrite env_filter_ne_cons_ne //.
-        iApply env_ltyped_cons. eauto with iFrame. }
+      - by rewrite ctx_filter_ne_cons.
+      - rewrite ctx_filter_ne_cons_ne //.
+        iApply ctx_ltyped_cons. eauto with iFrame. }
     iIntros (w) "[$ HΓ]".
-    iApply env_ltyped_app. iFrame "HΓ1eq". by iApply env_ltyped_delete.
+    iApply ctx_ltyped_app. iFrame "HΓ1eq". by iApply ctx_ltyped_delete.
   Qed.
 
   Lemma ltyped_recv Γ (x : string) A S :
     Γ !! x = Some (chan (<??> TY A; S))%lty →
-    Γ ⊨ recv x : A ⫤ env_cons x (chan S) Γ.
+    Γ ⊨ recv x : A ⫤ ctx_cons x (chan S) Γ.
   Proof.
-    iIntros (HΓx%env_lookup_perm) "!>". iIntros (vs) "HΓ /=".
+    iIntros (HΓx%ctx_lookup_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.
+    iDestruct (ctx_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs.
+    wp_recv (v) as "HA". iFrame "HA". iApply ctx_ltyped_cons; eauto with iFrame.
   Qed.
 
   Definition select : val := λ: "c" "i", send "c" "i".
@@ -93,13 +93,13 @@ Section session_typing_rules.
   Lemma ltyped_select Γ (x : string) (i : Z) (S : lsty Σ) Ss :
     Γ !! x = Some (chan (lty_select Ss))%lty →
     Ss !! i = Some S →
-    Γ ⊨ select x #i : () ⫤ env_cons x (chan S) Γ.
+    Γ ⊨ select x #i : () ⫤ ctx_cons x (chan S) Γ.
   Proof.
-    iIntros (HΓx%env_lookup_perm Hin); iIntros "!>" (vs) "HΓ /=".
+    iIntros (HΓx%ctx_lookup_perm Hin); iIntros "!>" (vs) "HΓ /=".
     rewrite {1}HΓx /=.
-    iDestruct (env_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs.
+    iDestruct (ctx_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Γ' /=".
+    iDestruct (ctx_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ") as "HΓ' /=".
     by rewrite insert_id // lookup_total_alt Hin.
   Qed.
 
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index b5aab7a..579423d 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -8,14 +8,14 @@ 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 Export environments.
+From actris.logrel Require Export contexts.
 From iris.proofmode Require Import tactics.
 
 (** The semantic typing judgment *)
 Definition ltyped `{!heapG Σ}
-    (Γ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.
+    (Γ1 Γ2 : ctx Σ) (e : expr) (A : ltty Σ) : iProp Σ :=
+  tc_opaque (■ ∀ vs, ctx_ltyped vs Γ1 -∗
+    WP subst_map vs e {{ v, ltty_car A v ∗ ctx_ltyped vs Γ2 }})%I.
 Instance: Params (@ltyped) 2 := {}.
 
 Notation "Γ1 ⊨ e : A ⫤ Γ2" := (ltyped Γ1 Γ2 e A)
@@ -98,6 +98,6 @@ Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
 Proof.
   intros Hty. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?.
   destruct (Hty _) as (A & He). iIntros "_".
-  iDestruct (He $!∅ with "[]") as "He"; first by rewrite /env_ltyped.
+  iDestruct (He $!∅ with "[]") as "He"; first by rewrite /ctx_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 3cb323e..8e69e9c 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -2,7 +2,6 @@
 these lemmas are semantic versions of the syntactic typing judgments typically
 found in a syntactic type system. *)
 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 par.
 From actris.logrel Require Export subtyping_rules term_typing_judgment operators.
@@ -11,7 +10,7 @@ From actris.channel Require Import proofmode.
 Section term_typing_rules.
   Context `{heapG Σ}.
   Implicit Types A B : ltty Σ.
-  Implicit Types Γ : env Σ.
+  Implicit Types Γ : ctx Σ.
 
   (** Frame rule *)
   Lemma ltyped_frame Γ Γ1 Γ2 e A :
@@ -19,26 +18,26 @@ Section term_typing_rules.
     (Γ1 ++ Γ ⊨ e : A ⫤ Γ2 ++ Γ).
   Proof.
     iIntros "#He !>" (vs) "HΓ".
-    iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 HΓ]".
+    iDestruct (ctx_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 "[$]").
+    iIntros (v) "[$ HΓ2]". by iApply (ctx_ltyped_app with "[$]").
   Qed.
 
   (** Variable properties *)
   Lemma ltyped_var Γ (x : string) A :
     Γ !! x = Some A →
-    Γ ⊨ x : A ⫤ env_cons x (copy- A) Γ.
+    Γ ⊨ x : A ⫤ ctx_cons x (copy- A) Γ.
   Proof.
-    iIntros (HΓx%env_lookup_perm) "!>"; iIntros (vs) "HΓ /=".
+    iIntros (HΓx%ctx_lookup_perm) "!>"; iIntros (vs) "HΓ /=".
     rewrite {1}HΓx /=.
-    iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]". rewrite Hvs.
+    iDestruct (ctx_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.
+    iApply wp_value. iFrame "HA". iApply ctx_ltyped_cons. eauto with iFrame.
   Qed.
 
   (** Subtyping *)
   Theorem ltyped_subsumption Γ1 Γ2 Γ1' Γ2' e τ τ' :
-    Γ1 <env: Γ1' -∗ τ' <: τ -∗ Γ2' <env: Γ2 -∗
+    Γ1 <ctx: Γ1' -∗ τ' <: τ -∗ Γ2' <ctx: Γ2 -∗
     (Γ1' ⊨ e : τ' ⫤ Γ2') -∗ (Γ1 ⊨ e : τ ⫤ Γ2).
   Proof.
     iIntros "#HleΓ1 #Hle #HleΓ2 #He" (vs) "!> HΓ1".
@@ -56,7 +55,7 @@ Section term_typing_rules.
     (Γ1 ⊨ e : τ ⫤ Γ2) -∗ (Γ1 ⊨ e : τ ⫤ []).
   Proof.
     iApply ltyped_subsumption;
-      [iApply env_le_refl|iApply lty_le_refl|iApply env_le_nil].
+      [iApply ctx_le_refl|iApply lty_le_refl|iApply ctx_le_nil].
   Qed.
 
   (** Basic properties *)
@@ -132,44 +131,44 @@ Section term_typing_rules.
   Qed.
 
   Lemma ltyped_lam Γ1 Γ2 x e A1 A2 :
-    (env_cons x A1 Γ1 ⊨ e : A2 ⫤ []) -∗
+    (ctx_cons x A1 Γ1 ⊨ e : A2 ⫤ []) -∗
     Γ1 ++ Γ2 ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ Γ2.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=". wp_pures.
-    iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 $]".
+    iDestruct (ctx_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'".
-    { by iApply (env_ltyped_insert' with "HA1"). }
+    { by iApply (ctx_ltyped_insert' with "HA1"). }
     rewrite subst_map_binder_insert.
     iApply (wp_wand with "He'"). by iIntros (w) "[$ _]".
   Qed.
 
   (* TODO: This might be derivable from rec value rule *)
   Lemma ltyped_val_lam x e A1 A2 :
-    (env_cons x A1 [] ⊨ e : A2 ⫤ []) -∗
+    (ctx_cons x A1 [] ⊨ e : A2 ⫤ []) -∗
     ⊨ᵥ (λ: x, e) : A1 ⊸ A2.
   Proof.
     iIntros "#He !>" (v) "HA1".
     wp_pures.
     iDestruct ("He" $!(binder_insert x v ∅) with "[HA1]") as "He'".
-    { iApply (env_ltyped_insert' ∅ ∅ x A1 v with "HA1").
-      iApply env_ltyped_nil. }
+    { iApply (ctx_ltyped_insert' ∅ ∅ x A1 v with "HA1").
+      iApply ctx_ltyped_nil. }
     rewrite subst_map_binder_insert /= binder_delete_empty subst_map_empty.
     iApply (wp_wand with "He'"). by iIntros (w) "[$ _]".
   Qed.
 
   (* Typing rule for introducing copyable functions *)
-  Definition env_copy_minus : env Σ → env Σ :=
-    fmap (λ xA, EnvItem (env_item_name xA) (lty_copy_minus  (env_item_type xA))).
+  Definition ctx_copy_minus : ctx Σ → ctx Σ :=
+    fmap (λ xA, CtxItem (ctx_item_name xA) (lty_copy_minus (ctx_item_type xA))).
 
   Lemma ltyped_rec Γ1 Γ2 f x e A1 A2 :
-    (env_cons f (A1 → A2) (env_cons x A1 (env_copy_minus Γ1)) ⊨ e : A2 ⫤ []) -∗
+    (ctx_cons f (A1 → A2) (ctx_cons x A1 (ctx_copy_minus Γ1)) ⊨ e : A2 ⫤ []) -∗
     Γ1 ++ Γ2 ⊨ (rec: f x := e) : A1 → A2 ⫤ Γ2.
   Proof.
     iIntros "#He". iIntros (vs) "!> HΓ /=". wp_pures.
-    iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 $]".
-    iAssert (<pers> env_ltyped vs (env_copy_minus Γ1))%I as "{HΓ1} #HΓ1".
-    { iClear "He". rewrite /env_copy_minus big_sepL_persistently big_sepL_fmap.
+    iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]".
+    iAssert (<pers> ctx_ltyped vs (ctx_copy_minus Γ1))%I as "{HΓ1} #HΓ1".
+    { iClear "He". rewrite /ctx_copy_minus big_sepL_persistently big_sepL_fmap.
       iApply (big_sepL_impl with "HΓ1"). iIntros "!>" (k [y B] _) "/=".
       iDestruct 1 as (v ?) "HB". iExists v. iSplit; [by auto|].
       by iDestruct (coreP_intro with "HB") as "{HB} #HB". }
@@ -177,24 +176,24 @@ Section term_typing_rules.
     iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
     iDestruct ("He" $! (binder_insert f r (binder_insert x v vs))
       with "[HΓ1 HA1]") as "He'".
-    { iApply (env_ltyped_insert' with "IH").
-      by iApply (env_ltyped_insert' with "HA1"). }
+    { iApply (ctx_ltyped_insert' with "IH").
+      by iApply (ctx_ltyped_insert' with "HA1"). }
     rewrite !subst_map_binder_insert_2.
     iApply (wp_wand with "He'"). iIntros (w) "[$ _]".
   Qed.
 
   Lemma ltyped_val_rec f x e A1 A2 :
-    (env_cons f (A1 → A2) (env_cons x A1 []) ⊨ e : A2 ⫤ []) -∗
+    (ctx_cons f (A1 → A2) (ctx_cons x A1 []) ⊨ e : A2 ⫤ []) -∗
     ⊨ᵥ (rec: f x := e) : A1 → A2.
   Proof.
     iIntros "#He". simpl. iLöb as "IH".
     iIntros (v) "!>!> HA1". wp_pures. set (r := RecV f x _).
     iDestruct ("He"$! (binder_insert f r (binder_insert x v ∅))
                  with "[HA1]") as "He'".
-    { iApply (env_ltyped_insert').
+    { iApply (ctx_ltyped_insert').
       { rewrite /ltyped_val /=. iApply "IH". }
-      iApply (env_ltyped_insert' with "HA1").
-      iApply env_ltyped_nil. }
+      iApply (ctx_ltyped_insert' with "HA1").
+      iApply ctx_ltyped_nil. }
     rewrite !subst_map_binder_insert_2 !binder_delete_empty subst_map_empty.
     iApply (wp_wand with "He'").
     iIntros (w) "[$ _]".
@@ -202,18 +201,18 @@ Section term_typing_rules.
 
   Lemma ltyped_let Γ1 Γ2 Γ3 x e1 e2 A1 A2 :
     (Γ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).
+    (ctx_cons x A1 Γ2 ⊨ e2 : A2 ⫤ Γ3) -∗
+    (Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ ctx_filter_eq x Γ2 ++ ctx_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.
-    rewrite {3}(env_filter_eq_perm Γ2 x).
-    iDestruct (env_ltyped_app with "HΓ2") as "[HΓ2eq HΓ2neq]".
+    rewrite {3}(ctx_filter_eq_perm Γ2 x).
+    iDestruct (ctx_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"). }
+    { by iApply (ctx_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.
+    iApply ctx_ltyped_app. iFrame "HΓ2eq". by iApply ctx_ltyped_delete.
   Qed.
 
   Lemma ltyped_seq Γ1 Γ2 Γ3 e1 e2 A B :
@@ -240,25 +239,25 @@ Section term_typing_rules.
 
   Lemma ltyped_fst Γ A1 A2 (x : string) :
     Γ !! x = Some (A1 * A2)%lty →
-    Γ ⊨ Fst x : A1 ⫤ env_cons x (copy- A1 * A2) Γ.
+    Γ ⊨ Fst x : A1 ⫤ ctx_cons x (copy- A1 * A2) Γ.
   Proof.
-    iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
-    iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
+    iIntros (HΓx%ctx_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (ctx_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Γ".
+    iFrame "HA1". iApply ctx_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 ⫤ env_cons x (A1 * copy- A2) Γ.
+    Γ ⊨ Snd x : A2 ⫤ ctx_cons x (A1 * copy- A2) Γ.
   Proof.
-    iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
-    iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
+    iIntros (HΓx%ctx_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (ctx_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Γ".
+    iFrame "HA2". iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ".
     iExists v1, v2. eauto with iFrame.
   Qed.
 
@@ -304,7 +303,7 @@ Section term_typing_rules.
     (Γ1 ++ Γ2 ⊨ (λ: <>, e) : (∀ X, C X) ⫤ Γ2).
   Proof.
     iIntros "#He" (vs) "!> HΓ /=". wp_pures.
-    iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 $]".
+    iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]".
     iIntros (M) "/=". wp_pures.
     iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[$ _]".
   Qed.
@@ -328,19 +327,19 @@ Section term_typing_rules.
 
   Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 x e1 e2 (C : lty Σ k → ltty Σ) B :
     (Γ1 ⊨ e1 : (∃ X, C X) ⫤ Γ2) -∗
-    (∀ K, env_cons x (C K) Γ2 ⊨ e2 : B ⫤ Γ3) -∗
-    (Γ1 ⊨ (let: x := e1 in e2) : B ⫤ env_filter_eq x Γ2 ++ env_filter_ne x Γ3).
+    (∀ K, ctx_cons x (C K) Γ2 ⊨ e2 : B ⫤ Γ3) -∗
+    (Γ1 ⊨ (let: x := e1 in e2) : B ⫤ ctx_filter_eq x Γ2 ++ ctx_filter_ne x Γ3).
   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.
-    rewrite {3}(env_filter_eq_perm Γ2 x).
-    iDestruct (env_ltyped_app with "HΓ2") as "[HΓ2eq HΓ2neq]".
+    rewrite {3}(ctx_filter_eq_perm Γ2 x).
+    iDestruct (ctx_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"). }
+    { by iApply (ctx_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.
+    iIntros (w) "[$ HΓ3]". iApply ctx_ltyped_app.
+    iFrame "HΓ2eq". by iApply ctx_ltyped_delete.
   Qed.
 
   (** Mutable Unique Reference properties *)
@@ -364,27 +363,27 @@ Section term_typing_rules.
 
   Lemma ltyped_load Γ (x : string) A :
     Γ !! x = Some (ref_uniq A)%lty →
-    Γ ⊨ ! x : A ⫤ env_cons x (ref_uniq (copy- A)) Γ.
+    Γ ⊨ ! x : A ⫤ ctx_cons x (ref_uniq (copy- A)) Γ.
   Proof.
-    iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
-    iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
+    iIntros (HΓx%ctx_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (ctx_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Γ".
+    iFrame "HA". iApply ctx_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 →
     (Γ ⊨ e : B ⫤ Γ') -∗
-    (Γ ⊨ x <- e : () ⫤ env_cons x (ref_uniq B) Γ').
+    (Γ ⊨ x <- e : () ⫤ ctx_cons x (ref_uniq B) Γ').
   Proof.
-    iIntros (HΓx%env_lookup_perm) "#He"; iIntros (vs) "!> HΓ /=".
+    iIntros (HΓx%ctx_lookup_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 (ctx_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Γ'".
+    iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ'".
     iExists l, v. eauto with iFrame.
   Qed.
 
@@ -454,10 +453,10 @@ Section term_typing_rules.
     (Γ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]".
+    iDestruct (ctx_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.
+    + iApply ctx_ltyped_app. by iFrame.
   Qed.
 End term_typing_rules.
-- 
GitLab