diff --git a/_CoqProject b/_CoqProject
index efc7341b2c2b579d56590226212569d045b44411..d075ea2a46a315bea641e69b0580edfc76bf0d19 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -28,6 +28,7 @@ theories/typing/type_incl.v
 theories/typing/perm.v
 theories/typing/typing.v
 theories/typing/lft_contexts.v
+theories/typing/type_context.v
 theories/typing/own.v
 theories/typing/uniq_bor.v
 theories/typing/shr_bor.v
diff --git a/opam.pins b/opam.pins
index 57d2788c63d2f4eb4779af0ea059b967ef0d4d1f..d6a8be766eafdbfa9679accc8a561e7889bafc1b 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2407263c14e0a44a8eafedcc2f5391b6c16ef1c4
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b72a3301d7ff957cfbb06d06bba85fb4ee9a2c39
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 0189938398f2dbc58668dc9107b832bed0527186..58e72cf04b57985773be26fa1f63d74df063dad9 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -4,13 +4,13 @@ From lrust.lang Require Export heap.
 From lrust.lang Require Import proofmode notation.
 
 Class heapPreG Σ := HeapPreG {
-  heap_preG_iris :> irisPreG lrust_lang Σ;
+  heap_preG_ownP :> ownPPreG lrust_lang Σ;
   heap_preG_heap :> inG Σ (authR heapUR);
   heap_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
 }.
 
 Definition heapΣ : gFunctors :=
-  #[irisΣ state;
+  #[ownPΣ state;
     GFunctor (constRF (authR heapUR));
     GFunctor (constRF (authR heap_freeableUR))].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
@@ -20,7 +20,7 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   (∀ `{heapG Σ}, {{ heap_ctx }} e {{ v, ⌜φ v⌝ }}) →
   adequate e σ φ.
 Proof.
-  intros Hwp; eapply (wp_adequacy Σ). iIntros (?) "Hσ".
+  intros Hwp; eapply (ownP_adequacy Σ _). iIntros (?) "Hσ".
   iMod (own_alloc (● to_heap σ)) as (vγ) "Hvγ".
   { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
   iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ"; first done.
diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index 04362d16b007e3bf233a5332101ed0eec929e601..5242e0cfd1121b1a12546b779eeddd80a1e766b3 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -16,7 +16,7 @@ Definition Newlft := Lit LitUnit.
 Definition Endlft := Skip.
 
 Section derived.
-Context `{irisG lrust_lang Σ}.
+Context `{ownPG lrust_lang Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 817a5bdb082bd36c8a451f5606ba488981c82434..82c5404f240617267aa10f32bfc53768b5c8ef3d 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -17,7 +17,7 @@ Definition heap_freeableUR : ucmraT :=
   gmapUR block (prodR fracR (gmapR Z (exclR unitC))).
 
 Class heapG Σ := HeapG {
-  heapG_iris_inG :> irisG lrust_lang Σ;
+  heapG_ownP_inG :> ownPG lrust_lang Σ;
   heap_inG :> inG Σ (authR heapUR);
   heap_freeable_inG :> inG Σ (authR heap_freeableUR);
   heap_name : gname;
@@ -403,7 +403,7 @@ Section heap.
     iIntros "H● H◯".
     iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
     iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
-    rewrite /to_heap lookup_fmap fmap_Some_setoid.
+    rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
     move=> /Some_pair_included_total_2
       [/Some_pair_included [_ Hincl] /to_agree_included->].
@@ -420,7 +420,7 @@ Section heap.
     iIntros "H● H◯".
     iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
     iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
-    rewrite /to_heap lookup_fmap fmap_Some_setoid.
+    rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
     apply (Some_included_exclusive _ _) in Hincl as [? Hval]; last by destruct ls''.
     apply (inj to_agree) in Hval. fold_leibniz. subst.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index c36762987b346b6ce926cf9e9f22ce192b579ff3..5810abc7d80fc38dd57ca961c3c6fc257e225e6c 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Export weakestpre ownp.
 From iris.program_logic Require Import ectx_lifting.
 From lrust.lang Require Export lang.
 From lrust.lang Require Import tactics.
@@ -6,8 +6,10 @@ From iris.proofmode Require Import tactics.
 Import uPred.
 Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
 
+(* TODO : as for heap_lang, directly use a global heap invariant. *)
+
 Section lifting.
-Context `{irisG lrust_lang Σ}.
+Context `{ownPG lrust_lang Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types ef : option expr.
 
@@ -30,7 +32,7 @@ Lemma wp_alloc_pst E σ n:
       ⌜∃ vl, n = length vl ∧ init_mem l vl σ = σ'⌝ ∗
       ownP σ' }}}.
 Proof.
-  iIntros (? Φ) "HP HΦ". iApply (wp_lift_atomic_head_step _ σ); eauto.
+  iIntros (? Φ) "HP HΦ". iApply (ownP_lift_atomic_head_step _ σ); eauto.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
   rewrite big_sepL_nil right_id. by iApply "HΦ"; iFrame; eauto.
 Qed.
@@ -41,7 +43,7 @@ Lemma wp_free_pst E σ l n :
   {{{ ▷ ownP σ }}} Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
   {{{ RET LitV $ LitUnit; ownP (free_mem l (Z.to_nat n) σ) }}}.
 Proof.
-  iIntros (???)  "HP HΦ". iApply (wp_lift_atomic_head_step _ σ); eauto.
+  iIntros (???)  "HP HΦ". iApply (ownP_lift_atomic_head_step _ σ); eauto.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
   rewrite big_sepL_nil right_id. by iApply "HΦ".
 Qed.
@@ -50,7 +52,7 @@ Lemma wp_read_sc_pst E σ l n v :
   σ !! l = Some (RSt n, v) →
   {{{ ▷ ownP σ }}} Read ScOrd (Lit $ LitLoc l) @ E {{{ RET v; ownP σ }}}.
 Proof.
-  iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
+  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
   by intros; inv_head_step; eauto using to_of_val.
   rewrite big_sepL_nil right_id; iFrame.
 Qed.
@@ -60,7 +62,7 @@ Lemma wp_read_na2_pst E σ l n v :
   {{{ ▷ ownP σ }}} Read Na2Ord (Lit $ LitLoc l) @ E
   {{{ RET v; ownP (<[l:=(RSt n, v)]>σ) }}}.
 Proof.
-  iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
+  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
   by intros; inv_head_step; eauto using to_of_val.
   rewrite big_sepL_nil right_id; iFrame.
 Qed.
@@ -72,7 +74,7 @@ Lemma wp_read_na1_pst E l Φ :
           WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }})) -∗
   WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
-  iIntros "HΦP". iApply (wp_lift_head_step E); auto.
+  iIntros "HΦP". iApply (ownP_lift_head_step E); auto.
   iMod "HΦP" as (σ n v) "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
   iNext. iIntros (e2 σ2 ef) "% HΦ". inv_head_step.
   rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
@@ -83,7 +85,7 @@ Lemma wp_write_sc_pst E σ l v v' :
   {{{ ▷ ownP σ }}} Write ScOrd (Lit $ LitLoc l) (of_val v) @ E
   {{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
 Proof.
-  iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
+  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
   by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
 Qed.
 
@@ -92,7 +94,7 @@ Lemma wp_write_na2_pst E σ l v v' :
   {{{ ▷ ownP σ }}} Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E
   {{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
 Proof.
-  iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
+  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
   by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
 Qed.
 
@@ -103,7 +105,7 @@ Lemma wp_write_na1_pst E l v Φ :
        WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }})) -∗
   WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
 Proof.
-  iIntros "HΦP". iApply (wp_lift_head_step E); auto.
+  iIntros "HΦP". iApply (ownP_lift_head_step E); auto.
   iMod "HΦP" as (σ v') "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
   iNext. iIntros (e2 σ2 ef) "% HΦ". inv_head_step.
   rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
@@ -120,7 +122,7 @@ Lemma wp_cas_pst E n σ l e1 lit1 lit2 litl :
       else ⌜lit_neq σ lit1 litl⌝ ∗ ownP σ }}}.
 Proof.
   iIntros (?%of_to_val ? Hdec Hn ?) "HP HΦ". subst.
-  iApply wp_lift_atomic_head_step; eauto.
+  iApply ownP_lift_atomic_head_step; eauto.
   { destruct Hdec as [Heq|Hneq].
     - specialize (Hn Heq). subst. do 3 eexists. by eapply CasSucS.
     - do 3 eexists. by eapply CasFailS. }
@@ -135,7 +137,7 @@ Qed.
 Lemma wp_fork E e :
   {{{ â–· WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitUnit; True }}}.
 Proof.
-  iIntros (?) "?HΦ". iApply wp_lift_pure_det_head_step; eauto.
+  iIntros (?) "?HΦ". iApply ownP_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto. iNext.
   rewrite big_sepL_singleton. iFrame. iApply wp_value. done. by iApply "HΦ".
 Qed.
@@ -148,7 +150,7 @@ Lemma wp_rec E e f xl erec erec' el Φ :
   ▷ WP subst' f e erec' @ E {{ Φ }} -∗
   WP App e el @ E {{ Φ }}.
 Proof.
-  iIntros (-> ???) "?". iApply wp_lift_pure_det_head_step; subst; eauto.
+  iIntros (-> ???) "?". iApply ownP_lift_pure_det_head_step; subst; eauto.
   by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
 Qed.
 
@@ -157,8 +159,8 @@ Lemma wp_bin_op_heap E σ op l1 l2 l' :
   {{{ ▷ ownP σ }}} BinOp op (Lit l1) (Lit l2) @ E
   {{{ l'', RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ ∗ ownP σ }}}.
 Proof.
-  iIntros (? Φ) "HP HΦ". iApply wp_lift_atomic_head_step; eauto.
-  iFrame "HP". iNext. iIntros (e2 σ2 efs Hs) "Ho". 
+  iIntros (? Φ) "HP HΦ". iApply ownP_lift_atomic_head_step; eauto.
+  iFrame "HP". iNext. iIntros (e2 σ2 efs Hs) "Ho".
   inv_head_step; rewrite big_sepL_nil right_id.
   iApply "HΦ". eauto.
 Qed.
@@ -168,9 +170,9 @@ Lemma wp_bin_op_pure E op l1 l2 l' :
   {{{ True }}} BinOp op (Lit l1) (Lit l2) @ E
   {{{ l'' σ, RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ }}}.
 Proof.
-  iIntros (? Φ) "HΦ". iApply wp_lift_pure_head_step; eauto.
+  iIntros (? Φ) "HΦ". iApply ownP_lift_pure_head_step; eauto.
   { intros. inv_head_step. done. }
-  iNext. iIntros (e2 efs σ Hs). 
+  iNext. iIntros (e2 efs σ Hs).
   inv_head_step; rewrite big_sepL_nil right_id.
   rewrite -wp_value //. iApply "HΦ". eauto.
 Qed.
@@ -180,7 +182,7 @@ Lemma wp_case E i e el Φ :
   nth_error el (Z.to_nat i) = Some e →
   ▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
 Proof.
-  iIntros (??) "?". iApply wp_lift_pure_det_head_step; eauto.
+  iIntros (??) "?". iApply ownP_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
 Qed.
 End lifting.
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 41440f80885f49316bf69aced25c7b94f22581cd..b53199cf4c0bc28ef62de0c67a927f3169de8ad4 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -3,7 +3,7 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import typing perm.
 
 Section bool.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Program Definition bool : type :=
     {| st_size := 1; st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]⌝)%I |}.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 7aa2e14d2575b5b6c601d22c4e755c17225abbe8..a23272ff51ff0d195bc5fd425cf35261914cfe19 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -5,7 +5,7 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import type_incl typing.
 
 Section fn.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
     {| ty_size := 1;
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 7c4f8c06d8c17352e8295097b9338e90c42cac78..ce2340bd2fda98f5be290df60a7488b572a90e91 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -3,7 +3,7 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import typing bool perm.
 
 Section int.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Program Definition int : type :=
     {| st_size := 1; st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]⌝)%I |}.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 88eb4bb8611565664a4daa529f01ab64d661e39a..a8a713acb89c44e186fc01a1149d3b90fce2bfb7 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -33,8 +33,8 @@ Section lft_contexts.
     AsFractional (lectx_interp E q) (lectx_interp E) q.
   Proof. done. Qed.
   Global Instance lectx_interp_permut:
-    Proper ((≡ₚ) ==> pointwise_relation _ (⊣⊢)) lectx_interp.
-  Proof. intros ????. by apply big_opL_permutation. Qed.
+    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) lectx_interp.
+  Proof. intros ????? ->. by apply big_opL_permutation. Qed.
   Typeclasses Opaque lectx_interp.
 
   (* Local lifetime contexts. *)
@@ -68,8 +68,8 @@ Section lft_contexts.
     AsFractional (llctx_interp L q) (llctx_interp L) q.
   Proof. done. Qed.
   Global Instance llctx_interp_permut:
-    Proper ((≡ₚ) ==> pointwise_relation _ (⊣⊢)) llctx_interp.
-  Proof. intros ????. by apply big_opL_permutation. Qed.
+    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) llctx_interp.
+  Proof. intros ????? ->. by apply big_opL_permutation. Qed.
   Typeclasses Opaque llctx_interp.
 
   Context (E : lectx) (L : llctx).
@@ -200,5 +200,4 @@ Section lft_contexts.
     iExists q. rewrite {1 2 4 5}/lectx_interp big_sepL_cons /=.
     iIntros "{$Hincl $HE'}!>[_ ?]". by iApply "Hclose'".
   Qed.
-
 End lft_contexts.
\ No newline at end of file
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 20c0cdf769442ddfc1e0f736e9b99a1fe0452be0..c0d98404057ee77d00b456dbc45cf3d53f324677 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -7,7 +7,7 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import typing product perm.
 
 Section own.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   (* Even though it does not seem too natural to put this here, it is
      the only place where it is used. *)
diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index e7effc6e8b8ca4d066a0792de0602d314aee8287..e7f1520023d3dff470264abc5dc1ed2c2fdb25c9 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -4,7 +4,7 @@ From lrust.lang Require Export proofmode notation.
 From lrust.lifetime Require Import borrow frac_borrow.
 
 Section perm.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Definition perm {Σ} := na_inv_pool_name → iProp Σ.
 
@@ -81,7 +81,7 @@ Notation "ρ1 ⇔ ρ2" := (equiv (A:=perm) ρ1%P ρ2%P)
 Notation "(⇔)" := (equiv (A:=perm)) (only parsing) : C_scope.
 
 Section duplicable.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Class Duplicable (ρ : @perm Σ) :=
     duplicable_persistent tid : PersistentP (ρ tid).
@@ -102,7 +102,7 @@ Section duplicable.
 End duplicable.
 
 Section has_type.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Lemma has_type_value (v : val) ty tid :
     (v ◁ ty)%P tid ⊣⊢ ty.(ty_own) tid [v].
@@ -118,7 +118,7 @@ Section has_type.
     WP ν @ E {{ Φ }}.
   Proof.
     iIntros "H◁ HΦ". setoid_rewrite has_type_value. unfold has_type.
-    destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]". simpl.
+    destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]".
     iMod ("HΦ" $! v with "[] H◁") as "HΦ". done.
     iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
       forall (Φ v EQν); try done.
@@ -130,7 +130,7 @@ Section has_type.
 End has_type.
 
 Section perm_incl.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   (* Properties *)
   Global Instance perm_incl_preorder : PreOrder (⇒).
diff --git a/theories/typing/product.v b/theories/typing/product.v
index e9aae329386d1af5e7d7b918160960196cab2be1..5acd25fb2d3d97c887c97d2d874474e495bf7d41 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -4,7 +4,7 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import perm type_incl.
 
 Section product.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Program Definition unit : type :=
     {| st_size := 0; st_own tid vl := ⌜vl = []⌝%I |}.
@@ -122,7 +122,7 @@ Arguments product : simpl never.
 Notation Π := product.
 
 Section typing.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   (* FIXME : do we still need this (flattening and unflattening)? *)
 
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 826b7249f9d0c0596a20d1c5c5a6a3474547464b..b60bff2faf17f127913010e90b1a1dfbb15460b3 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -5,7 +5,7 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import type_incl typing product own uniq_bor shr_bor.
 
 Section product_split.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Fixpoint combine_offs (tyl : list type) (accu : nat) :=
     match tyl with
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 7a06f36d7900e769644d4bd14b127f3c477633d5..13e15a5d11d52ce25139830cb941d70614f3f789 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -1,10 +1,10 @@
 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import frac_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import perm lft_contexts typing own uniq_bor.
+From lrust.typing Require Import perm lft_contexts type_context typing own uniq_bor.
 
 Section shr_bor.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Program Definition shr_bor (κ : lft) (ty : type) : type :=
     {| st_size := 1;
@@ -42,7 +42,7 @@ Notation "&shr{ κ } ty" := (shr_bor κ ty)
   (format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
 
 Section typing.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Lemma perm_incl_share q ν κ ty :
     ν ◁ &uniq{κ} ty ∗ q.[κ] ⇒ ν ◁ &shr{κ} ty ∗ q.[κ].
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 6d8039904168650c17e3fc465fa34c91e5c898f7..fa7968718a8a3edfded14d66e971ef931d3786c0 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -4,7 +4,7 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import type_incl.
 
 Section sum.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   (* [emp] cannot be defined using [ty_of_st], because the least we
      would be able to prove from its [ty_shr] would be [â–· False], but
@@ -123,7 +123,7 @@ Notation "Σ[ ty1 ; .. ; tyn ]" :=
   (sum (cons ty1 (..(cons tyn nil)..))) : lrust_type_scope.
 
 Section incl.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Lemma ty_incl_emp ρ ty : ty_incl ρ ∅ ty.
   Proof. iIntros (tid) "_ _!>". iSplit; iIntros "!#*/=[]". Qed.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index d40dc121c94d004717f92dadd1a8a407388bfe46..4d212d8c97a4ae8855ac748dcb2509e30c16a233 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -3,7 +3,7 @@ From lrust.lang Require Import heap.
 From lrust.lifetime Require Import borrow frac_borrow reborrow.
 From lrust.typing Require Import lft_contexts.
 
-Class iris_typeG Σ := Iris_typeG {
+Class typeG Σ := TypeG {
   type_heapG :> heapG Σ;
   type_lftG :> lftG Σ;
   type_na_invG :> na_invG Σ;
@@ -14,7 +14,7 @@ Definition mgmtE := ↑lftN.
 Definition lrustN := nroot .@ "lrust".
 
 Section type.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Definition thread_id := na_inv_pool_name.
 
@@ -55,7 +55,7 @@ Section type.
   (* We are repeating the typeclass parameter here jsut to make sure
      that simple_type does depend on it. Otherwise, the coercion defined
      bellow will not be acceptable by Coq. *)
-  Record simple_type `{iris_typeG Σ} :=
+  Record simple_type `{typeG Σ} :=
     { st_size : nat;
       st_own : thread_id → list val → iProp Σ;
 
@@ -111,16 +111,16 @@ Delimit Scope lrust_type_scope with T.
 Bind Scope lrust_type_scope with type.
 
 Section subtyping.
-  Context `{iris_typeG Σ} (E : lectx) (L : llctx).
+  Context `{typeG Σ} (E : lectx) (L : llctx).
 
   Record subtype (ty1 ty2 : type) : Prop :=
     { subtype_sz : ty1.(ty_size) = ty2.(ty_size);
       subtype_own qE qL :
         lft_ctx -∗ lectx_interp E qE -∗ llctx_interp L qL -∗
-          □ ∀ tid vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl;
+          □ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl;
       subtype_shr qE qL :
         lft_ctx -∗ lectx_interp E qE -∗ llctx_interp L qL -∗
-          □ ∀ κ tid F l, ty1.(ty_shr) κ tid F l → ty2.(ty_shr) κ tid F l }.
+          □ ∀ κ tid F l, ty1.(ty_shr) κ tid F l -∗ ty2.(ty_shr) κ tid F l }.
 
   Global Instance subtype_preorder : PreOrder subtype.
   Proof.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
new file mode 100644
index 0000000000000000000000000000000000000000..b23985b01284529b3ffc088e9054ba4abf75f716
--- /dev/null
+++ b/theories/typing/type_context.v
@@ -0,0 +1,115 @@
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import big_op.
+From lrust.lang Require Import notation.
+From lrust.lifetime Require Import definitions.
+From lrust.typing Require Import type lft_contexts.
+
+Section type_context.
+  Context `{typeG Σ}.
+
+  Definition path := expr.
+
+  Fixpoint eval_path (ν : path) : option val :=
+    match ν with
+    | BinOp OffsetOp e (Lit (LitInt n)) =>
+      match eval_path e with
+      | Some (#(LitLoc l)) => Some (#(shift_loc l n))
+      | _ => None
+      end
+    | e => to_val e
+    end.
+
+  Inductive tctx_elt : Type :=
+  | TCtx_holds (p : path) (ty : type)
+  | TCtx_guarded (p : path) (κ : lft) (ty : type).
+  Definition tctx := list tctx_elt.
+
+  Definition tctx_elt_interp (tid : thread_id) (x : tctx_elt) : iProp Σ :=
+    match x with
+    | TCtx_holds p ty => ∃ v, ⌜eval_path p = Some v⌝ ∗ ty.(ty_own) tid [v]
+    | TCtx_guarded p κ ty => ∃ v, ⌜eval_path p = Some v⌝ ∗
+        ∀ E, ⌜↑lftN ⊆ E⌝ -∗ [†κ] ={E}=∗ ▷ ty.(ty_own) tid [v]
+    end%I.
+  Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
+    ([∗ list] x ∈ T, tctx_elt_interp tid x)%I.
+
+  Global Instance tctx_interp_permut:
+    Proper (eq ==> (≡ₚ) ==> (⊣⊢)) tctx_interp.
+  Proof. intros ?? -> ???. by apply big_opL_permutation. Qed.
+
+  Definition tctx_incl (E : lectx) (L : llctx) (T1 T2 : tctx): Prop :=
+    ∀ qE qL, lft_ctx -∗ lectx_interp E qE -∗ llctx_interp L qL -∗
+          □ ∀ tid, tctx_interp tid T1 -∗ tctx_interp tid T2.
+
+  Global Instance tctx_incl_preorder E L : PreOrder (tctx_incl E L).
+  Proof.
+    split.
+    - by iIntros (???) "_ _ _ !# * $".
+    - iIntros (??? H1 H2 ??) "#LFT HE HL".
+      iDestruct (H1 with "LFT HE HL") as "#H1".
+      iDestruct (H2 with "LFT HE HL") as "#H2".
+      iIntros "{HE HL}!# * H". iApply "H2". by iApply "H1".
+  Qed.
+
+  Lemma contains_tctx_incl E L T1 T2 : T1 `contains` T2 → tctx_incl E L T2 T1.
+  Proof.
+    rewrite /tctx_incl. iIntros (EQ ??) "_ _ _ !# * H". by iApply big_sepL_contains.
+  Qed.
+
+  Lemma tctx_incl_frame E L T T1 T2 :
+    tctx_incl E L T2 T1 → tctx_incl E L (T++T2) (T++T1).
+  Proof.
+    iIntros (Hincl ??) "#LFT HE HL". rewrite /tctx_interp.
+    iDestruct (Hincl with "LFT HE HL") as"#Hincl".
+    iIntros "{HE HL} !# *". rewrite !big_sepL_app.
+    iIntros "[$ ?]". by iApply "Hincl".
+  Qed.
+
+  Lemma copy_tctx_incl E L p `(!Copy ty) :
+    tctx_incl E L [TCtx_holds p ty] [TCtx_holds p ty; TCtx_holds p ty].
+  Proof.
+    iIntros (??) "_ _ _ !# *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
+    by iIntros "[#$ $]".
+  Qed.
+
+  Lemma subtype_tctx_incl E L p ty1 ty2 :
+    subtype E L ty1 ty2 → tctx_incl E L [TCtx_holds p ty1] [TCtx_holds p ty2].
+  Proof.
+    iIntros (Hst ??) "#LFT HE HL".
+    iDestruct (subtype_own _ _ _ _ Hst with "LFT HE HL") as "#Hst".
+    iIntros "{HE HL} !# * H". rewrite /tctx_interp !big_sepL_singleton /=.
+    iDestruct "H" as (v) "[% H]". iExists _. iFrame "%". by iApply "Hst".
+  Qed.
+
+  Definition deguard_tctx_elt κ x :=
+    match x with
+    | TCtx_guarded p κ' ty =>
+      if decide (κ = κ') then TCtx_holds p ty else x
+    | _ => x
+    end.
+
+  Lemma deguard_tctx_elt_interp tid E κ x :
+    ↑lftN ⊆ E → [†κ] -∗ tctx_elt_interp tid x ={E}=∗
+        ▷ tctx_elt_interp tid (deguard_tctx_elt κ x).
+  Proof.
+    iIntros (?) "H† H". destruct x as [|? κ' ?]; simpl. by auto.
+    destruct (decide (κ = κ')) as [->|]; simpl; last by auto.
+    iDestruct "H" as (v) "[% H]". iExists v. iSplitR. by auto.
+    by iApply ("H" with "[] H†").
+  Qed.
+
+  Definition deguard_tctx κ (T : tctx) : tctx :=
+    deguard_tctx_elt κ <$> T.
+
+  Lemma deguard_tctx_interp tid E κ T :
+    ↑lftN ⊆ E → [†κ] -∗ tctx_interp tid T ={E}=∗
+        ▷ tctx_interp tid (deguard_tctx κ T).
+  Proof.
+    iIntros (?) "#H† H". rewrite /tctx_interp big_sepL_fmap.
+    iApply (big_opL_forall (λ P Q, [†κ] -∗ P ={E}=∗ ▷ Q) with "H† H").
+    { by iIntros (?) "_ $". }
+    { iIntros (?? A ?? B) "#H† [H1 H2]". iSplitL "H1".
+        by iApply (A with "H†"). by iApply (B with "H†"). }
+    move=>/= _ ? _. by apply deguard_tctx_elt_interp.
+  Qed.
+End type_context.
\ No newline at end of file
diff --git a/theories/typing/type_incl.v b/theories/typing/type_incl.v
index 2bae7738ef1b882f813a74e55b4ea7f9258f9097..3752887487da76aef96beff949f7216cfabf12fa 100644
--- a/theories/typing/type_incl.v
+++ b/theories/typing/type_incl.v
@@ -4,7 +4,7 @@ From lrust.typing Require Export type perm.
 From lrust.lifetime Require Import frac_borrow borrow.
 
 Section ty_incl.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
     ∀ tid, lft_ctx -∗ ρ tid ={⊤}=∗
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 6d5fdc3efb2aebf0e1cda9b9fddb00a3377f5774..d092e01f24a1cb9d32025fd51b4ca5f980c468f6 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -7,7 +7,7 @@ From lrust.lang Require Import proofmode.
 From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 
 Section typing.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
   Definition typed_step (ρ : perm) e (θ : val → perm) :=
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index ad6ca09c690bbd5cd351448d0b540a3b76512e89..94c3f5ee9c72fcd79003c0350d0d4a795cc21f9f 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -5,7 +5,7 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import perm lft_contexts typing own.
 
 Section uniq_bor.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Program Definition uniq_bor (κ:lft) (ty:type) :=
     {| ty_size := 1;
@@ -103,7 +103,7 @@ Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
   (format "&uniq{ κ } ty", at level 20, right associativity) : lrust_type_scope.
 
 Section typing.
-  Context `{iris_typeG Σ}.
+  Context `{typeG Σ}.
 
   Lemma own_uniq_borrowing ν q ty κ :
     borrowing κ ⊤ (ν ◁ own q ty) (ν ◁ &uniq{κ} ty).