From 2851d1244cf21dad58e265b1c858ed04eb6816bd Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 13 Dec 2016 19:07:25 +0100
Subject: [PATCH] Continuations, function type, and its variance.

---
 _CoqProject                     |   1 +
 theories/lang/heap.v            |   4 +-
 theories/lifetime/primitive.v   |   6 +-
 theories/typing/function.v      | 177 +++++++++++++-------------------
 theories/typing/lft_contexts.v  | 157 ++++++++++++++++++----------
 theories/typing/own.v           |  12 +--
 theories/typing/perm.v          |  24 -----
 theories/typing/product.v       |  20 ++--
 theories/typing/product_split.v |   2 +-
 theories/typing/shr_bor.v       |  20 ++--
 theories/typing/sum.v           |  57 +++++-----
 theories/typing/type.v          |  42 +++++---
 theories/typing/type_context.v  |  39 +++----
 theories/typing/type_incl.v     |   7 --
 theories/typing/typing.v        |  26 ++++-
 theories/typing/uniq_bor.v      |  22 ++--
 16 files changed, 307 insertions(+), 309 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index d075ea2a..49f8db42 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -29,6 +29,7 @@ theories/typing/perm.v
 theories/typing/typing.v
 theories/typing/lft_contexts.v
 theories/typing/type_context.v
+theories/typing/cont_context.v
 theories/typing/own.v
 theories/typing/uniq_bor.v
 theories/typing/shr_bor.v
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 82c5404f..b0e3d4b1 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -124,7 +124,7 @@ Section heap.
   Qed.
   Global Instance heap_mapsto_as_fractional l q v:
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
-  Proof. done. Qed.
+  Proof. split. done. apply _. Qed.
 
   Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦∗{q} vl).
   Proof. rewrite /heap_mapsto_vec. apply _. Qed.
@@ -136,7 +136,7 @@ Section heap.
   Qed.
   Global Instance heap_mapsto_vec_as_fractional l q vl:
     AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
-  Proof. done. Qed.
+  Proof. split. done. apply _. Qed.
 
   Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
   Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index a7c48a0a..235510a1 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -278,7 +278,7 @@ Proof.
 Qed.
 Global Instance lft_tok_as_fractional κ q :
   AsFractional q.[κ] (λ q, q.[κ])%I q.
-Proof. done. Qed.
+Proof. split. done. apply _. Qed.
 Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
 Proof.
   intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
@@ -286,7 +286,7 @@ Proof.
 Qed.
 Global Instance idx_bor_own_as_fractional i q :
   AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
-Proof. done. Qed.
+Proof. split. done. apply _. Qed.
 
 (** Lifetime inclusion *)
 Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
@@ -355,7 +355,7 @@ Qed.
 (** Basic rules about borrows *)
 Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
 Proof.
-  rewrite /bor /raw_bor /idx_bor /bor_idx. iProof; iSplit.
+  rewrite /bor /raw_bor /idx_bor /bor_idx. iSplit.
   - iDestruct 1 as (κ') "[? Hraw]". iDestruct "Hraw" as (s) "[??]".
     iExists (κ', s). by iFrame.
   - iDestruct 1 as ([κ' s]) "[[??]?]".
diff --git a/theories/typing/function.v b/theories/typing/function.v
index c04fe440..510130ca 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -1,123 +1,88 @@
+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import hoare.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import type_incl typing.
+From lrust.typing Require Import type_incl typing lft_contexts type_context cont_context.
 
 Section fn.
   Context `{typeG Σ}.
 
-  Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
-    {| ty_size := 1;
-       ty_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗
-          ∀ vl, ρ vl tid -∗ na_own tid ⊤
-                 -∗ WP f (map of_val vl) {{λ _, False}})%I;
-       ty_shr κ tid N l := True%I |}.
-  Next Obligation.
-    iIntros (n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
-  Qed.
-  Next Obligation. intros. by iIntros "_ _". Qed.
-  Next Obligation. intros. by iIntros "_ _ _". Qed.
-
-  (* TODO : For now, functions are not Send. This means they cannot be
-     called in another thread than the one that created it.  We will
-     need Send functions when dealing with multithreading ([fork]
-     needs a Send closure). *)
-  Program Definition fn {A n} (ρ : A -> vec val n → @perm Σ) : type :=
+  Program Definition fn {A n} (E : A → elctx)
+          (tys : A → vec type n) (ty : A → type) : type :=
     {| st_size := 1;
-       st_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗ ∀ x vl,
-         {{ ρ x vl tid ∗ na_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
+       st_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗ □ ∀ (x : A) (args : vec val n) (k : val),
+         typed_body (E x) []
+                    [CctxElt k [] 1 (λ v, [TCtx_holds (v!!!0) (ty x)])]
+                    (zip_with (TCtx_holds ∘ of_val) args (tys x))
+                    (f (of_val <$> (args : list val))))%I |}.
   Next Obligation.
-    iIntros (x n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
-  Qed.
-
-  Lemma ty_incl_cont {n} ρ ρ1 ρ2 :
-    Duplicable ρ → (∀ vl : vec val n, ρ ∗ ρ2 vl ⇒ ρ1 vl) →
-    ty_incl ρ (cont ρ1) (cont ρ2).
-  Proof.
-    iIntros (? Hρ1ρ2 tid) "#LFT #Hρ!>". iSplit; iIntros "!#*H"; last by auto.
-    iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-    iIntros (vl) "Hρ2 Htl". iApply ("Hwp" with ">[-Htl] Htl").
-    iApply (Hρ1ρ2 with "LFT"). by iFrame.
-  Qed.
-
-  Lemma ty_incl_fn {A n} ρ ρ1 ρ2 :
-    Duplicable ρ → (∀ (x : A) (vl : vec val n), ρ ∗ ρ2 x vl ⇒ ρ1 x vl) →
-    ty_incl ρ (fn ρ1) (fn ρ2).
-  Proof.
-    iIntros (? Hρ1ρ2 tid) "#LFT #Hρ!>". iSplit; iIntros "!#*#H".
-    - iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-      iIntros (x vl) "!#[Hρ2 Htl]". iApply ("Hwp" with ">").
-      iFrame. iApply (Hρ1ρ2 with "LFT"). by iFrame.
-    - iSplit; last done. simpl. iDestruct "H" as (vl0) "[? [Hvl|H†]]".
-      + iExists vl0. iFrame "#". iLeft. iNext. iDestruct "Hvl" as (f) "[% Hwp]".
-        iExists f. iSplit. done. iIntros (x vl) "!#[Hρ2 Htl]".
-        iApply ("Hwp" with ">"). iFrame. iApply (Hρ1ρ2 with "LFT >"). by iFrame.
-      + iExists _. iFrame "#". by iRight.
-  Qed.
-
-  Lemma ty_incl_fn_cont {A n} ρ ρf (x : A) :
-    ty_incl ρ (fn ρf) (cont (n:=n) (ρf x)).
-  Proof.
-    iIntros (tid) "#LFT _!>". iSplit; iIntros "!#*H"; last by iSplit.
-    iDestruct "H" as (f) "[%#H]". subst. iExists _. iSplit. done.
-    iIntros (vl) "Hρf Htl". iApply "H". by iFrame.
+    iIntros (A n E tys ty tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
 
-  Lemma ty_incl_fn_specialize {A B n} (f : A → B) ρ ρfn :
-    ty_incl ρ (fn (n:=n) ρfn) (fn (ρfn ∘ f)).
+  Lemma fn_subtype_ty A n E0 E L tys1 tys2 ty1 ty2:
+    (∀ x, Forall2 (subtype (E0 ++ E x) L) (tys2 x : vec _ _) (tys1 x : vec _ _)) →
+    (∀ x, subtype (E0 ++ E x) L (ty1 x) (ty2 x)) →
+    subtype E0 L (@fn A n E tys1 ty1) (@fn A n E tys2 ty2).
   Proof.
-    iIntros (tid) "_ _!>". iSplit; iIntros "!#*H".
-    - iDestruct "H" as (fv) "[%#H]". subst. iExists _. iSplit. done.
-      iIntros (x vl). by iApply "H".
-    - iSplit; last done.
-      iDestruct "H" as (fvl) "[?[Hown|H†]]".
-      + iExists _. iFrame. iLeft. iNext.
-        iDestruct "Hown" as (fv) "[%H]". subst. iExists _. iSplit. done.
-        iIntros (x vl). by iApply "H".
-      + iExists _. iFrame. by iRight.
+    intros Htys Hty. apply subtype_simple_type=>//=.
+    iIntros (_ ?) "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
+    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * _ HE HL HC HT".
+    iDestruct (elctx_interp_persist with "HE") as "#HE'".
+    iApply ("Hf" with "* LFT HE HL [HC] [HT]").
+    - iIntros "HE". unfold cctx_interp. iIntros (e) "He".
+      iDestruct "He" as %->%elem_of_list_singleton. iIntros (ret) "HL HT".
+      iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
+      iApply ("HC" $! (CctxElt _ _ _ _) with "[%] * HL >").
+        by apply elem_of_list_singleton.
+      iApply (subtype_tctx_incl with "LFT [HE0] HL0 HT"). by apply Hty.
+      rewrite /elctx_interp_0 big_sepL_app. by iSplit.
+    - rewrite /tctx_interp
+         -(fst_zip (tys1 x) (tys2 x)) ?vec_to_list_length //
+         -{1}(snd_zip (tys1 x) (tys2 x)) ?vec_to_list_length //
+         !zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
+      iApply big_sepL_impl. iSplit; last done. iIntros "{HT}!#".
+      iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
+      iDestruct "H" as (v) "[? Hown]". iExists v. iFrame.
+      rewrite !lookup_zip_with.
+      iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 &
+        (? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some.
+      specialize (Htys x). eapply Forall2_lookup_lr in Htys; try done.
+      iApply (Htys.(subtype_own _ _ _ _) with "LFT [] HL0 Hown").
+      rewrite /elctx_interp_0 big_sepL_app. by iSplit.
   Qed.
 
-  Lemma typed_fn {A n} `{Duplicable _ ρ, Closed (f :b: xl +b+ []) e} θ :
-    length xl = n →
-    (∀ (a : A) (vl : vec val n) (fv : val) e',
-        subst_l xl (map of_val vl) e = Some e' →
-        typed_program (fv ◁ fn θ ∗ (θ a vl) ∗ ρ) (subst' f fv e')) →
-    typed_step_ty ρ (Rec f xl e) (fn θ).
-  Proof.
-    iIntros (Hn He tid) "!#(#HEAP&#LFT&#Hρ&$)".
-    assert (Rec f xl e = RecV f xl e) as -> by done. iApply wp_value'.
-    rewrite has_type_value.
-    iLöb as "IH". iExists _. iSplit. done. iIntros (a vl) "!#[Hθ?]".
-    assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He'].
-    { clear -Hn. revert xl Hn e. induction vl=>-[|x xl] //=. by eauto.
-      intros ? e. edestruct IHvl as [e' ->]. congruence. eauto. }
-    iApply wp_rec; try done.
-    { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
-      rewrite to_of_val. eauto. }
-    iNext. iApply He. done. iFrame "∗#". by rewrite has_type_value.
-  Qed.
+  (* Lemma ty_incl_fn_specialize {A B n} (f : A → B) ρ ρfn : *)
+  (*   ty_incl ρ (fn (n:=n) ρfn) (fn (ρfn ∘ f)). *)
+  (* Proof. *)
+  (*   iIntros (tid) "_ _!>". iSplit; iIntros "!#*H". *)
+  (*   - iDestruct "H" as (fv) "[%#H]". subst. iExists _. iSplit. done. *)
+  (*     iIntros (x vl). by iApply "H". *)
+  (*   - iSplit; last done. *)
+  (*     iDestruct "H" as (fvl) "[?[Hown|H†]]". *)
+  (*     + iExists _. iFrame. iLeft. iNext. *)
+  (*       iDestruct "Hown" as (fv) "[%H]". subst. iExists _. iSplit. done. *)
+  (*       iIntros (x vl). by iApply "H". *)
+  (*     + iExists _. iFrame. by iRight. *)
+  (* Qed. *)
 
-  Lemma typed_cont {n} `{Closed (f :b: xl +b+ []) e} ρ θ :
-    length xl = n →
-    (∀ (fv : val) (vl : vec val n) e',
-        subst_l xl (map of_val vl) e = Some e' →
-        typed_program (fv ◁ cont (λ vl, ρ ∗ θ vl)%P ∗ (θ vl) ∗ ρ) (subst' f fv e')) →
-    typed_step_ty ρ (Rec f xl e) (cont θ).
-  Proof.
-    iIntros (Hn He tid) "!#(#HEAP&#LFT&Hρ&$)". specialize (He (RecV f xl e)).
-    assert (Rec f xl e = RecV f xl e) as -> by done. iApply wp_value'.
-    rewrite has_type_value.
-    iLöb as "IH". iExists _. iSplit. done. iIntros (vl) "Hθ ?".
-    assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He'].
-    { clear -Hn. revert xl Hn e. induction vl=>-[|x xl] //=. by eauto.
-      intros ? e. edestruct IHvl as [e' ->]. congruence. eauto. }
-    iApply wp_rec; try done.
-    { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
-      rewrite to_of_val. eauto. }
-    iNext. iApply He. done. iFrame "∗#". rewrite has_type_value.
-    iExists _. iSplit. done. iIntros (vl') "[Hρ Hθ] Htl".
-    iDestruct ("IH" with "Hρ") as (f') "[Hf' IH']".
-    iDestruct "Hf'" as %[=<-]. iApply ("IH'" with "Hθ Htl").
-  Qed.
+  (* Lemma typed_fn {A n} `{Duplicable _ ρ, Closed (f :b: xl +b+ []) e} θ : *)
+  (*   length xl = n → *)
+  (*   (∀ (a : A) (vl : vec val n) (fv : val) e', *)
+  (*       subst_l xl (map of_val vl) e = Some e' → *)
+  (*       typed_program (fv ◁ fn θ ∗ (θ a vl) ∗ ρ) (subst' f fv e')) → *)
+  (*   typed_step_ty ρ (Rec f xl e) (fn θ). *)
+  (* Proof. *)
+  (*   iIntros (Hn He tid) "!#(#HEAP&#LFT&#Hρ&$)". *)
+  (*   assert (Rec f xl e = RecV f xl e) as -> by done. iApply wp_value'. *)
+  (*   rewrite has_type_value. *)
+  (*   iLöb as "IH". iExists _. iSplit. done. iIntros (a vl) "!#[Hθ?]". *)
+  (*   assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He']. *)
+  (*   { clear -Hn. revert xl Hn e. induction vl=>-[|x xl] //=. by eauto. *)
+  (*     intros ? e. edestruct IHvl as [e' ->]. congruence. eauto. } *)
+  (*   iApply wp_rec; try done. *)
+  (*   { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]]. *)
+  (*     rewrite to_of_val. eauto. } *)
+  (*   iNext. iApply He. done. iFrame "∗#". by rewrite has_type_value. *)
+  (* Qed. *)
 End fn.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index a8a713ac..a1665a3f 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -9,33 +9,63 @@ Section lft_contexts.
 
   (* External lifetime contexts. *)
 
-  Inductive lectx_elt : Type :=
-  | LECtx_Alive κ
-  | LECtx_Incl κ κ'.
-  Definition lectx := list lectx_elt.
+  Inductive elctx_elt : Type :=
+  | ELCtx_Alive κ
+  | ELCtx_Incl κ κ'.
+  Definition elctx := list elctx_elt.
 
-  Definition lectx_elt_interp (x : lectx_elt) (q : Qp) : iProp Σ :=
+  Definition elctx_elt_interp (x : elctx_elt) (q : Qp) : iProp Σ :=
     match x with
-    | LECtx_Alive κ => q.[κ]
-    | LECtx_Incl κ κ' => κ ⊑ κ'
+    | ELCtx_Alive κ => q.[κ]
+    | ELCtx_Incl κ κ' => κ ⊑ κ'
     end%I.
-  Global Instance lectx_elt_interp_fractional x:
-    Fractional (lectx_elt_interp x).
-  Proof. destruct x; unfold lectx_elt_interp; apply _. Qed.
-  Typeclasses Opaque lectx_elt_interp.
-
-  Definition lectx_interp (E : lectx) (q : Qp) : iProp Σ :=
-    ([∗ list] x ∈ E, lectx_elt_interp x q)%I.
-  Global Instance lectx_interp_fractional E:
-    Fractional (lectx_interp E).
+  Global Instance elctx_elt_interp_fractional x:
+    Fractional (elctx_elt_interp x).
+  Proof. destruct x; unfold elctx_elt_interp; apply _. Qed.
+  Typeclasses Opaque elctx_elt_interp.
+  Definition elctx_elt_interp_0 (x : elctx_elt) : iProp Σ :=
+    match x with
+    | ELCtx_Alive κ => True
+    | ELCtx_Incl κ κ' => κ ⊑ κ'
+    end%I.
+  Global Instance elctx_elt_interp_0_persistent x:
+    PersistentP (elctx_elt_interp_0 x).
+  Proof. destruct x; apply _. Qed.
+  Typeclasses Opaque elctx_elt_interp_0.
+
+  Lemma elctx_elt_interp_persist x q :
+    elctx_elt_interp x q -∗ elctx_elt_interp_0 x.
+  Proof. destruct x; by iIntros "?/=". Qed.
+
+  Definition elctx_interp (E : elctx) (q : Qp) : iProp Σ :=
+    ([∗ list] x ∈ E, elctx_elt_interp x q)%I.
+  Global Instance elctx_interp_fractional E:
+    Fractional (elctx_interp E).
   Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
-  Global Instance lectx_interp_as_fractional E q:
-    AsFractional (lectx_interp E q) (lectx_interp E) q.
-  Proof. done. Qed.
-  Global Instance lectx_interp_permut:
-    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) lectx_interp.
+  Global Instance elctx_interp_as_fractional E q:
+    AsFractional (elctx_interp E q) (elctx_interp E) q.
+  Proof. split. done. apply _. Qed.
+  Global Instance elctx_interp_permut:
+    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) elctx_interp.
   Proof. intros ????? ->. by apply big_opL_permutation. Qed.
-  Typeclasses Opaque lectx_interp.
+  Typeclasses Opaque elctx_interp.
+
+  Definition elctx_interp_0 (E : elctx) : iProp Σ :=
+    ([∗ list] x ∈ E, elctx_elt_interp_0 x)%I.
+  Global Instance elctx_interp_0_persistent E:
+    PersistentP (elctx_interp_0 E).
+  Proof. apply _. Qed.
+  Global Instance elctx_interp_0_permut:
+    Proper ((≡ₚ) ==> (⊣⊢)) elctx_interp_0.
+  Proof. intros ???. by apply big_opL_permutation. Qed.
+  Typeclasses Opaque elctx_interp_0.
+
+  Lemma elctx_interp_persist x q :
+    elctx_interp x q -∗ elctx_interp_0 x.
+  Proof.
+    unfold elctx_interp, elctx_interp_0. f_equiv. intros _ ?.
+    apply elctx_elt_interp_persist.
+  Qed.
 
   (* Local lifetime contexts. *)
 
@@ -59,6 +89,15 @@ Section lft_contexts.
   Qed.
   Typeclasses Opaque llctx_elt_interp.
 
+  Definition llctx_elt_interp_0 (x : llctx_elt) : Prop :=
+    let κ' := foldr (∪) static (x.2) in (∃ κ0, x.1 = κ' ∪ κ0).
+  Lemma llctx_elt_interp_persist x q :
+    llctx_elt_interp x q -∗ ⌜llctx_elt_interp_0 x⌝.
+  Proof.
+    iIntros "H". unfold llctx_elt_interp.
+    iDestruct "H" as (κ0) "[% _]". by iExists κ0.
+  Qed.
+
   Definition llctx_interp (L : llctx) (q : Qp) : iProp Σ :=
     ([∗ list] x ∈ L, llctx_elt_interp x q)%I.
   Global Instance llctx_interp_fractional L:
@@ -66,13 +105,22 @@ Section lft_contexts.
   Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
   Global Instance llctx_interp_as_fractional L q:
     AsFractional (llctx_interp L q) (llctx_interp L) q.
-  Proof. done. Qed.
+  Proof. split. done. apply _. Qed.
   Global Instance llctx_interp_permut:
     Proper ((≡ₚ) ==> eq ==> (⊣⊢)) llctx_interp.
   Proof. intros ????? ->. by apply big_opL_permutation. Qed.
   Typeclasses Opaque llctx_interp.
 
-  Context (E : lectx) (L : llctx).
+  Definition llctx_interp_0 (L : llctx) : Prop :=
+    ∀ x, x ∈ L → llctx_elt_interp_0 x.
+  Lemma llctx_interp_persist L q :
+    llctx_interp L q -∗ ⌜llctx_interp_0 L⌝.
+  Proof.
+    iIntros "H". iIntros (x ?). iApply llctx_elt_interp_persist.
+    unfold llctx_interp. by iApply (big_sepL_elem_of with "H").
+  Qed.
+
+  Context (E : elctx) (L : llctx).
 
   (* Lifetime inclusion *)
 
@@ -80,40 +128,39 @@ Section lft_contexts.
      "equivalence" of lifetimes. If so, TODO : add it, and the
      corresponding [Proper] instances for the relevent types. *)
   Definition incl κ κ' : Prop :=
-    ∀ qE qL, lectx_interp E qE -∗ llctx_interp L qL -∗ κ ⊑ κ'.
+    elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ κ ⊑ κ'.
 
   Global Instance incl_preorder : PreOrder incl.
   Proof.
     split.
-    - iIntros (???) "_ _". iApply lft_incl_refl.
-    - iIntros (??? H1 H2 ??) "HE HL". iApply (lft_incl_trans with "[#] [#]").
+    - iIntros (?) "_ _". iApply lft_incl_refl.
+    - iIntros (??? H1 H2) "#HE #HL". iApply (lft_incl_trans with "[#] [#]").
       iApply (H1 with "HE HL"). iApply (H2 with "HE HL").
   Qed.
 
   Lemma incl_static κ : incl κ static.
-  Proof. iIntros (??) "_ _". iApply lft_incl_static. Qed.
+  Proof. iIntros "_ _". iApply lft_incl_static. Qed.
 
   Lemma incl_local κ κ' κs : (κ, κs) ∈ L → κ' ∈ κs → incl κ κ'.
   Proof.
-    intros ? Hκ'κs ??. rewrite /llctx_interp /llctx_elt_interp big_sepL_elem_of //.
-    iIntros "_ H". iDestruct "H" as (κ0) "[H _]". simpl. iDestruct "H" as %->.
+    iIntros (? Hκ'κs) "_ H". iDestruct "H" as %(κ0 & EQ). done. simpl in EQ; subst.
     iApply lft_le_incl. etrans; last by apply gmultiset_union_subseteq_l.
     clear -Hκ'κs. induction Hκ'κs.
     - apply gmultiset_union_subseteq_l.
     - etrans. done. apply gmultiset_union_subseteq_r.
   Qed.
 
-  Lemma incl_external κ κ' : LECtx_Incl κ κ' ∈ E → incl κ κ'.
+  Lemma incl_external κ κ' : ELCtx_Incl κ κ' ∈ E → incl κ κ'.
   Proof.
-    intros ???. rewrite /lectx_interp /lectx_elt_interp big_sepL_elem_of //.
-      by iIntros "$ _".
+    iIntros (?) "H _".
+    rewrite /elctx_interp_0 /elctx_elt_interp_0 big_sepL_elem_of //. done.
   Qed.
 
   (* Lifetime aliveness *)
 
   Definition alive (κ : lft) : Prop :=
-    ∀ F qE qL, ⌜↑lftN ⊆ F⌝ -∗ lectx_interp E qE -∗ llctx_interp L qL ={F}=∗
-          ∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ lectx_interp E qE ∗ llctx_interp L qL).
+    ∀ F qE qL, ⌜↑lftN ⊆ F⌝ -∗ elctx_interp E qE -∗ llctx_interp L qL ={F}=∗
+          ∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ elctx_interp E qE ∗ llctx_interp L qL).
 
   Lemma alive_static : alive static.
   Proof.
@@ -127,7 +174,7 @@ Section lft_contexts.
     iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done.
     iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
     iAssert (∃ q', q'.[foldr union static κs] ∗
-      (q'.[foldr union static κs] ={F}=∗ lectx_interp E qE ∗ llctx_interp L (qL / 2)))%I
+      (q'.[foldr union static κs] ={F}=∗ elctx_interp E qE ∗ llctx_interp L (qL / 2)))%I
       with ">[HE HL1]" as "H".
     { move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
       iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
@@ -147,10 +194,10 @@ Section lft_contexts.
     rewrite /llctx_interp /llctx_elt_interp. iApply "Hclose". iExists κ0. iFrame. auto.
   Qed.
 
-  Lemma alive_lectx κ: LECtx_Alive κ ∈ E → alive κ.
+  Lemma alive_elctx κ: ELCtx_Alive κ ∈ E → alive κ.
   Proof.
     iIntros ([i HE]%elem_of_list_lookup_1 F qE qL) "% HE $ !>".
-    rewrite /lectx_interp /lectx_elt_interp.
+    rewrite /elctx_interp /elctx_elt_interp.
     iDestruct (big_sepL_lookup_acc with "HE") as "[Hκ Hclose]". done.
     iExists qE. iFrame. iIntros "?!>". by iApply "Hclose".
   Qed.
@@ -158,7 +205,8 @@ Section lft_contexts.
   Lemma alive_incl κ κ': alive κ → incl κ κ' → alive κ'.
   Proof.
     iIntros (Hal Hinc F qE qL) "% HE HL".
-    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". by iApply (Hinc with "HE HL").
+    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hinc with "[HE] [HL]").
+      by iApply elctx_interp_persist. by iApply llctx_interp_persist.
     iMod (Hal with "[%] HE HL") as (q') "[Htok Hclose]". done.
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose']". done.
     iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with ">").
@@ -167,37 +215,38 @@ Section lft_contexts.
 
   (* External lifetime context satisfiability *)
 
-  Definition lectx_sat E' : Prop :=
-    ∀ qE qL F, ⌜↑lftN ⊆ F⌝ -∗ lectx_interp E qE -∗ llctx_interp L qL ={F}=∗
-      ∃ qE', lectx_interp E' qE' ∗
-       (lectx_interp E' qE' ={F}=∗ lectx_interp E qE ∗ llctx_interp L qL).
+  Definition elctx_sat E' : Prop :=
+    ∀ qE qL F, ⌜↑lftN ⊆ F⌝ -∗ elctx_interp E qE -∗ llctx_interp L qL ={F}=∗
+      ∃ qE', elctx_interp E' qE' ∗
+       (elctx_interp E' qE' ={F}=∗ elctx_interp E qE ∗ llctx_interp L qL).
 
-  Lemma lectx_sat_nil : lectx_sat [].
+  Lemma elctx_sat_nil : elctx_sat [].
   Proof.
-    iIntros (qE qL F) "%$$". iExists 1%Qp. rewrite /lectx_interp big_sepL_nil. auto.
+    iIntros (qE qL F) "%$$". iExists 1%Qp. rewrite /elctx_interp big_sepL_nil. auto.
   Qed.
 
-  Lemma lectx_sat_alive E' κ :
-    alive κ → lectx_sat E' → lectx_sat (LECtx_Alive κ :: E').
+  Lemma elctx_sat_alive E' κ :
+    alive κ → elctx_sat E' → elctx_sat (ELCtx_Alive κ :: E').
   Proof.
     iIntros (Hκ HE' qE qL F) "% [HE1 HE2] [HL1 HL2]".
     iMod (Hκ with "[%] HE1 HL1") as (q) "[Htok Hclose]". done.
     iMod (HE' with "[%] HE2 HL2") as (q') "[HE' Hclose']". done.
     destruct (Qp_lower_bound q q') as (q0 & q2 & q'2 & -> & ->). iExists q0.
-    rewrite {5 6}/lectx_interp big_sepL_cons /=.
+    rewrite {5 6}/elctx_interp big_sepL_cons /=.
     iDestruct "Htok" as "[$ Htok]". iDestruct "HE'" as "[Hf HE']".
-    iSplitL "Hf". by rewrite /lectx_interp.
+    iSplitL "Hf". by rewrite /elctx_interp.
     iIntros "!>[Htok' ?]". iMod ("Hclose" with "[$Htok $Htok']") as "[$$]".
-    iApply "Hclose'". iFrame. by rewrite /lectx_interp.
+    iApply "Hclose'". iFrame. by rewrite /elctx_interp.
   Qed.
 
-  Lemma lectx_sat_incl E' κ κ' :
-    incl κ κ' → lectx_sat E' → lectx_sat (LECtx_Incl κ κ' :: E').
+  Lemma elctx_sat_incl E' κ κ' :
+    incl κ κ' → elctx_sat E' → elctx_sat (ELCtx_Incl κ κ' :: E').
   Proof.
     iIntros (Hκκ' HE' qE qL F) "% HE HL".
-    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". by iApply (Hκκ' with "HE HL").
+    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hκκ' with "[HE] [HL]").
+      by iApply elctx_interp_persist. by iApply llctx_interp_persist.
     iMod (HE' with "[%] HE HL") as (q) "[HE' Hclose']". done.
-    iExists q. rewrite {1 2 4 5}/lectx_interp big_sepL_cons /=.
+    iExists q. rewrite {1 2 4 5}/elctx_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 983739b3..aaf7b21d 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -104,21 +104,17 @@ Section own.
   Proof.
     intros ty1 ty2 Hincl. split.
     - done.
-    - iIntros (qE qL) "#LFT HE HL *".
-      iDestruct (Hincl.(subtype_own _ _ _ _) with "LFT HE HL") as "#Howni".
-      iIntros "{HE HL} !# * H". iDestruct "H" as (l) "(%&Hmt&H†)". subst.
+    - iIntros (??) "#LFT #HE #HL H". iDestruct "H" as (l) "(%&Hmt&H†)". subst.
       iExists _. iSplit. done. iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
       iDestruct (ty_size_eq with "Hown") as %<-.
-      iDestruct ("Howni" with "* Hown") as "Hown".
+      iDestruct (Hincl.(subtype_own _ _ _ _) with "LFT HE HL Hown") as "Hown".
       iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
       iExists _. by iFrame.
-    - iIntros (qE qL) "#LFT HE HL *".
-      iDestruct (Hincl.(subtype_shr _ _ _ _) with "LFT HE HL") as "#Hshri".
-      iIntros "{HE HL} !# * H". iDestruct "H" as (l') "[Hfb #Hvs]".
+    - iIntros (????) "#LFT #HE #HL H". iDestruct "H" as (l') "[Hfb #Hvs]".
       iExists l'. iFrame. iIntros "!#". iIntros (F') "%".
       iMod ("Hvs" with "* [%]") as "Hvs'". done. iModIntro. iNext.
       iMod "Hvs'" as "[Hshr|H†]"; last by auto.
-      iLeft. iApply ("Hshri" with "* Hshr").
+      iLeft. iApply (Hincl.(subtype_shr _ _ _ _) with "LFT HE HL Hshr").
   Qed.
 
   Global Instance own_proper E L n :
diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index 39206bea..2d6e434d 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -80,27 +80,6 @@ Notation "ρ1 ⇔ ρ2" := (equiv (A:=perm) ρ1%P ρ2%P)
    (at level 95, no associativity) : C_scope.
 Notation "(⇔)" := (equiv (A:=perm)) (only parsing) : C_scope.
 
-Section duplicable.
-  Context `{typeG Σ}.
-
-  Class Duplicable (ρ : @perm Σ) :=
-    duplicable_persistent tid : PersistentP (ρ tid).
-  Global Existing Instance duplicable_persistent.
-
-  Global Instance has_type_dup v ty : Copy ty → Duplicable (v ◁ ty).
-  Proof. intros Hdup tid. apply _. Qed.
-
-  Global Instance lft_incl_dup κ κ' : Duplicable (κ ⊑ κ').
-  Proof. intros tid. apply _. Qed.
-
-  Global Instance sep_dup P Q :
-    Duplicable P → Duplicable Q → Duplicable (P ∗ Q).
-  Proof. intros HP HQ tid. apply _. Qed.
-
-  Global Instance top_dup : Duplicable ⊤.
-  Proof. intros tid. apply _. Qed.
-End duplicable.
-
 Section has_type.
   Context `{typeG Σ}.
 
@@ -189,9 +168,6 @@ Section perm_incl.
   Global Instance perm_top_left_id : LeftId (⇔) ⊤ sep.
   Proof. intros ρ. by rewrite comm right_id. Qed.
 
-  Lemma perm_incl_duplicable ρ (_ : Duplicable ρ) : ρ ⇒ ρ ∗ ρ.
-  Proof. iIntros (tid) "_ #H!>". by iSplit. Qed.
-
   Lemma perm_tok_plus κ q1 q2 :
     tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
   Proof. rewrite /tok /sep /=; split; by iIntros (tid) "_ [$$]". Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index df7fde17..0933c519 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -59,17 +59,15 @@ Section product.
   Proof.
     iIntros (ty11 ty12 H1 ty21 ty22 H2). split.
     - by rewrite /= (subtype_sz _ _ _ _ H1) (subtype_sz _ _ _ _ H2).
-    - iIntros (??) "#LFT HE HL".
-      iDestruct (subtype_own _ _ _ _ H1 with "LFT HE HL") as "#H1".
-      iDestruct (subtype_own _ _ _ _ H2 with "LFT HE HL") as "#H2".
-      iIntros "{HE HL}!# * H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
-      iExists _, _. iSplit. done. by iSplitL "Hown1"; [iApply "H1"|iApply "H2"].
-    - iIntros (??) "#LFT HE HL".
-      iDestruct (subtype_shr _ _ _ _ H1 with "LFT HE HL") as "#H1".
-      iDestruct (subtype_shr _ _ _ _ H2 with "LFT HE HL") as "#H2".
-      iIntros "{HE HL}!# * H". iDestruct "H" as (vl1 vl2) "(% & #Hshr1 & #Hshr2)".
-      iExists _, _. iSplit. done. erewrite subtype_sz; last done.
-      by iSplit; [iApply "H1"|iApply "H2"].
+    - iIntros (??) "#LFT #HE #HL H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
+      iExists _, _. iSplit. done. iSplitL "Hown1".
+      by iApply (H1.(subtype_own _ _ _ _) with "LFT HE HL").
+      by iApply (H2.(subtype_own _ _ _ _) with "LFT HE HL").
+    - iIntros (????) "#LFT #HE #HL H".
+      iDestruct "H" as (vl1 vl2) "(% & #Hshr1 & #Hshr2)".
+      iExists _, _. iSplit. done. erewrite subtype_sz; last done. iSplit.
+      by iApply (H1.(subtype_shr _ _ _ _) with "LFT HE HL").
+      by iApply (H2.(subtype_shr _ _ _ _) with "LFT HE HL").
   Qed.
   Global Instance product2_proper E L:
     Proper (eqtype E L ==> eqtype E L ==> eqtype E L) product2.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index b60bff2f..a39ce0e6 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -2,7 +2,7 @@ From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import type_incl typing product own uniq_bor shr_bor.
+From lrust.typing Require Import typing type_context perm product own uniq_bor shr_bor.
 
 Section product_split.
   Context `{typeG Σ}.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 4ec050d8..ee647288 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -18,19 +18,11 @@ Section shr_bor.
   Global Instance subtype_shr_bor_mono E L :
     Proper (flip (incl E L) ==> subtype E L ==> subtype E L) shr_bor.
   Proof.
-    intros κ1 κ2 Hκ ty1 ty2 Hty. split.
-    - done.
-    - iIntros (qE qL) "#LFT HE HL *". iDestruct (Hκ with "HE HL") as "#Hκ".
-      iDestruct (subtype_shr _ _ _ _ Hty with "LFT HE HL") as "#Hty".
-      iIntros "{HE HL}!#*H". iDestruct "H" as (l) "(% & H)". subst. iExists _.
-      iSplit. done. by iApply (ty2.(ty_shr_mono) with "LFT Hκ"); last iApply "Hty".
-    - iIntros (qE qL) "#LFT HE HL *". iDestruct (Hκ with "HE HL") as "#Hκ".
-      iDestruct (subtype_shr _ _ _ _ Hty with "LFT HE HL") as "#Hst".
-      iIntros "{HE HL}!#*H". iDestruct "H" as (vl) "#[Hfrac [Hty|H†]]".
-      + iExists vl. iFrame "#". iLeft. iNext. simpl.
-        iDestruct "Hty" as (l0) "(% & Hty)". subst. iExists _. iSplit. done.
-          by iApply (ty_shr_mono with "LFT Hκ"); last iApply "Hst".
-      + simpl. eauto.
+    intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type. done.
+    iIntros (??) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
+    iDestruct "H" as (l) "(% & H)". subst. iExists _. iSplit. done.
+    iApply (ty2.(ty_shr_mono) with "LFT Hκ"). reflexivity.
+    by iApply (Hty.(subtype_shr _ _ _ _ ) with "LFT HE HL").
   Qed.
   Global Instance subtype_shr_bor_mono' E L :
     Proper (incl E L ==> flip (subtype E L) ==> flip (subtype E L)) shr_bor.
@@ -49,7 +41,7 @@ Section typing.
   Lemma tctx_incl_share E L p κ ty :
     tctx_incl E L [TCtx_holds p (&uniq{κ}ty)] [TCtx_holds p (&shr{κ}ty)].
   Proof.
-    iIntros (??) "#LFT _ _ !# * Huniq". rewrite /tctx_interp !big_sepL_singleton /=.
+    iIntros (?) "#LFT _ _ Huniq". rewrite /tctx_interp !big_sepL_singleton /=.
     iDestruct "Huniq" as (v) "[% Huniq]". iExists _. iFrame "%".
     iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
     iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 82c649be..c707306a 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -115,32 +115,33 @@ Section incl.
   Proof.
   Admitted.
 
-  Lemma ty_incl_sum ρ n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) :
-    Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 →
-    ty_incl ρ (sum tyl1) (sum tyl2).
-  Proof.
-    iIntros (DUP FA tid) "#LFT #Hρ". rewrite /sum /=. iSplitR "".
-    - assert (Hincl : lft_ctx -∗ ρ tid ={⊤}=∗
-         (□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl
-                  → (nth i tyl2 ∅%T).(ty_own) tid vl)).
-      { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
-        - iIntros "_ _!>*!#". eauto.
-        - iIntros "#LFT #Hρ". iMod (IH with "LFT Hρ") as "#IH".
-          iMod (Hincl with "LFT Hρ") as "[#Hh _]".
-          iIntros "!>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
-      iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H".
-      iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
-        by iApply "Hincl".
-    - assert (Hincl : lft_ctx -∗ ρ tid ={⊤}=∗
-         (□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l
-                     → (nth i tyl2 ∅%T).(ty_shr) κ tid E l)).
-      { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
-        - iIntros "#LFT _!>*!#". eauto.
-        - iIntros "#LFT #Hρ".
-          iMod (IH with "LFT Hρ") as "#IH". iMod (Hincl with "LFT Hρ") as "[_ #Hh]".
-          iIntros "!>*!#*Hown". destruct i as [|i]; last by iApply "IH".
-          by iDestruct ("Hh" $! _ _ _ with "Hown") as "[$ _]". }
-      iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H". iSplit; last done.
-      iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
-  Qed.
+  (* TODO *)
+  (* Lemma ty_incl_sum ρ n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) : *)
+  (*   Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 → *)
+  (*   ty_incl ρ (sum tyl1) (sum tyl2). *)
+  (* Proof. *)
+  (*   iIntros (DUP FA tid) "#LFT #Hρ". rewrite /sum /=. iSplitR "". *)
+  (*   - assert (Hincl : lft_ctx -∗ ρ tid ={⊤}=∗ *)
+  (*        (□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl *)
+  (*                 → (nth i tyl2 ∅%T).(ty_own) tid vl)). *)
+  (*     { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH]. *)
+  (*       - iIntros "_ _!>*!#". eauto. *)
+  (*       - iIntros "#LFT #Hρ". iMod (IH with "LFT Hρ") as "#IH". *)
+  (*         iMod (Hincl with "LFT Hρ") as "[#Hh _]". *)
+  (*         iIntros "!>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". } *)
+  (*     iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H". *)
+  (*     iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done. *)
+  (*       by iApply "Hincl". *)
+  (*   - assert (Hincl : lft_ctx -∗ ρ tid ={⊤}=∗ *)
+  (*        (□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l *)
+  (*                    → (nth i tyl2 ∅%T).(ty_shr) κ tid E l)). *)
+  (*     { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH]. *)
+  (*       - iIntros "#LFT _!>*!#". eauto. *)
+  (*       - iIntros "#LFT #Hρ". *)
+  (*         iMod (IH with "LFT Hρ") as "#IH". iMod (Hincl with "LFT Hρ") as "[_ #Hh]". *)
+  (*         iIntros "!>*!#*Hown". destruct i as [|i]; last by iApply "IH". *)
+  (*         by iDestruct ("Hh" $! _ _ _ with "Hown") as "[$ _]". } *)
+  (*     iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H". iSplit; last done. *)
+  (*     iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl". *)
+  (* Qed. *)
 End incl.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 39ca984e..6ad88ebc 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -117,31 +117,29 @@ Delimit Scope lrust_type_scope with T.
 Bind Scope lrust_type_scope with type.
 
 Section subtyping.
-  Context `{typeG Σ} (E : lectx) (L : llctx).
+  Context `{typeG Σ} (E : elctx) (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;
-      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 }.
+      subtype_own tid vl:
+        lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
+           ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl;
+      subtype_shr κ tid F l:
+        lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
+           ty1.(ty_shr) κ tid F l -∗ ty2.(ty_shr) κ tid F l }.
 
   Global Instance subtype_preorder : PreOrder subtype.
   Proof.
     split.
-    - intros ty. split; [done| |]; iIntros (? ?) "_ _ _ !# * $".
+    - intros ty. split; [done|intros|intros]; iIntros "_ _ _ $".
     - intros ty1 ty2 ty3 H1 H2. split.
       + etrans. eapply H1. eapply H2.
-      + iIntros (? ?) "#LFT HE HL".
-        iDestruct (subtype_own _ _ H1 with "LFT HE HL") as "#H1".
-        iDestruct (subtype_own _ _ H2 with "LFT HE HL") as "#H2".
-        iIntros "{HE HL} !# * ?". iApply "H2". by iApply "H1".
-      + iIntros (? ?) "#LFT HE HL".
-        iDestruct (subtype_shr _ _ H1 with "LFT HE HL") as "#H1".
-        iDestruct (subtype_shr _ _ H2 with "LFT HE HL") as "#H2".
-        iIntros "{HE HL} !# * ?". iApply "H2". by iApply "H1".
+      + iIntros (??) "#LFT #HE #HL * H".
+        iApply (H2.(subtype_own _ _) with "LFT HE HL *").
+        by iApply (H1.(subtype_own _ _) with "LFT HE HL *").
+      + iIntros (????) "#LFT #HE #HL * H".
+        iApply (H2.(subtype_shr _ _) with "LFT HE HL *").
+        by iApply (H1.(subtype_shr _ _) with "LFT HE HL *").
   Qed.
 
   Definition eqtype (ty1 ty2 : type) : Prop :=
@@ -154,4 +152,16 @@ Section subtyping.
     - intros ?? Heq; split; apply Heq.
     - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
   Qed.
+
+  Lemma subtype_simple_type (st1 st2 : simple_type) :
+    st1.(st_size) = st2.(st_size) →
+    (∀ tid vl, lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
+                 st1.(st_own) tid vl -∗ st2.(st_own) tid vl) →
+    subtype st1 st2.
+  Proof.
+    intros Hsz Hst. split; [done|by apply Hst|].
+    iIntros (????) "#LFT #HE #HL H /=".
+    iDestruct "H" as (vl) "[Hf [Hown|H†]]"; iExists vl; iFrame "Hf"; last by auto.
+    iLeft. by iApply (Hst with "LFT HE HL *").
+  Qed.
 End subtyping.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 7d4bce1f..8114339d 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -33,52 +33,47 @@ Section type_context.
   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.
+  Global Instance tctx_interp_permut tid:
+    Proper ((≡ₚ) ==> (⊣⊢)) (tctx_interp tid).
+  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.
+  Definition tctx_incl (E : elctx) (L : llctx) (T1 T2 : tctx): Prop :=
+    ∀ tid, lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
+              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" with ">"). by iApply "H1".
+    - by iIntros (??) "_ _ _ $".
+    - iIntros (??? H1 H2 ?) "#LFT #HE #HL H".
+      iApply (H2 with "LFT HE HL >"). by iApply (H1 with "LFT HE HL").
   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.
+    rewrite /tctx_incl. iIntros (Hc ?) "_ _ _ 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".
+    intros Hincl ?. rewrite /tctx_interp !big_sepL_app. iIntros "#LFT #HE #HL [$ ?]".
+    by iApply (Hincl with "LFT HE HL").
   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.
+    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".
+    iIntros (Hst ?) "#LFT #HE #HL H". rewrite /tctx_interp !big_sepL_singleton /=.
+    iDestruct "H" as (v) "[% H]". iExists _. iFrame "%".
+    by iApply (Hst.(subtype_own _ _ _ _) with "LFT HE HL").
   Qed.
 
   Definition deguard_tctx_elt κ x :=
@@ -112,4 +107,4 @@ Section type_context.
         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
+End type_context.
diff --git a/theories/typing/type_incl.v b/theories/typing/type_incl.v
index 37528874..4cd87f37 100644
--- a/theories/typing/type_incl.v
+++ b/theories/typing/type_incl.v
@@ -35,13 +35,6 @@ Section ty_incl.
     iIntros (Hρθ Hρ' tid) "#LFT H". iApply (Hρ' with "LFT>"). iApply (Hρθ with "LFT H").
   Qed.
 
-  Global Instance ty_incl_preorder ρ: Duplicable ρ → PreOrder (ty_incl ρ).
-  Proof.
-    split.
-    - iIntros (ty tid) "_ _!>". iSplit; iIntros "!#"; eauto.
-    - eauto using ty_incl_weaken, ty_incl_trans, perm_incl_duplicable.
-  Qed.
-
   Lemma ty_incl_perm_incl ρ ty1 ty2 ν :
     ty_incl ρ ty1 ty2 → ρ ∗ ν ◁ ty1 ⇒ ν ◁ ty2.
   Proof.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index d092e01f..1eeb4fe6 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -2,13 +2,37 @@ From iris.program_logic Require Import hoare.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Export notation memcpy.
 From lrust.typing Require Export type.
-From lrust.typing Require Import perm.
+From lrust.typing Require Import perm lft_contexts type_context cont_context.
 From lrust.lang Require Import proofmode.
 From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 
 Section typing.
   Context `{typeG Σ}.
 
+  Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
+                        (e : expr) : iProp Σ :=
+    (∀ tid qE, lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗
+               (elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
+               WP e {{ _, cont_postcondition }})%I.
+
+  Instance typed_body_llctx_permut E :
+    Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
+  Proof.
+    intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body. by setoid_rewrite HL.
+  Qed.
+
+  Instance typed_body_mono E L:
+    Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢)) (typed_body E L).
+  Proof.
+    intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
+    iIntros (tid qE) "#LFT HE HL HC HT".
+    iMod (HT with "LFT [#] [#] HT") as "HT".
+      by iApply elctx_interp_persist. by iApply llctx_interp_persist.
+    iApply ("H" with "LFT HE HL [HC] HT").
+    iIntros "HE". iApply (HC with "LFT [#]").
+    by iApply elctx_interp_persist. by iApply "HC".
+  Qed.
+
   (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
   Definition typed_step (ρ : perm) e (θ : val → perm) :=
     ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ na_own tid ⊤ }} e
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index d4971ab9..362db405 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -68,27 +68,25 @@ Section uniq_bor.
   Proof.
     intros κ1 κ2 Hκ ty1 ty2 [Hty1 Hty2]. split.
     - done.
-    - iIntros (qE qL) "#LFT HE HL *". iDestruct (Hκ with "HE HL") as "#Hκ".
-      iDestruct (subtype_own _ _ _ _ Hty1 with "LFT HE HL") as "#Hty1".
-      iDestruct (subtype_own _ _ _ _ Hty2 with "LFT HE HL") as "#Hty2".
-      iIntros "{HE HL} !# * H". iDestruct "H" as (l P) "[[% #HPiff] Hown]". subst.
+    - iIntros (??) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
+      iDestruct "H" as (l P) "[[% #HPiff] Hown]". subst.
       iExists _, _. iSplitR; last by iApply (bor_shorten with "Hκ"). iSplit. done.
       iIntros "!#". iSplit; iIntros "H".
       + iDestruct ("HPiff" with "H") as (vl) "[??]". iExists vl. iFrame.
-        by iApply "Hty1".
+        by iApply (Hty1.(subtype_own _ _ _ _) with "LFT HE HL").
       + iDestruct "H" as (vl) "[??]". iApply "HPiff". iExists vl. iFrame.
-        by iApply "Hty2".
-    - iIntros (qE qL) "#LFT HE HL *". iDestruct (Hκ with "HE HL") as "#Hκ".
-      iDestruct (subtype_shr _ _ _ _ Hty1 with "LFT HE HL") as "#Hty".
-      iIntros "{HE HL} !# * H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
+        by iApply (Hty2.(subtype_own _ _ _ _) with "LFT HE HL").
+    - iIntros (????) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
+      iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
       { iApply (lft_incl_glb with "[] []").
         - iApply (lft_incl_trans with "[] Hκ"). iApply lft_le_incl.
-            apply gmultiset_union_subseteq_l.
+          apply gmultiset_union_subseteq_l.
         - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
       iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!#%%".
       iMod ("Hupd" with "* [%]") as "Hupd'"; try done. iModIntro. iNext.
       iMod "Hupd'" as "[H|H†]"; last by auto.
-      iLeft. iApply (ty_shr_mono with "LFT Hincl'"); last by iApply "Hty". done.
+      iLeft. iApply (ty_shr_mono with "LFT Hincl'"). reflexivity.
+      by iApply (Hty1.(subtype_shr _ _ _ _) with "LFT HE HL").
   Qed.
   Global Instance subtype_uniq_mono' E L :
     Proper (incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
@@ -222,4 +220,4 @@ Section typing.
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv.
     iExists _, _. erewrite <-uPred.iff_refl. auto.
   Qed.
-End typing.
\ No newline at end of file
+End typing.
-- 
GitLab