diff --git a/_CoqProject b/_CoqProject
index d1abaecb5c75999104693f66ec2a50cb95207d2c..2935afb5580998904c2319e797d469779b066d96 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -24,7 +24,6 @@ theories/lang/races.v
 theories/lang/tactics.v
 theories/lang/wp_tactics.v
 theories/typing/type.v
-theories/typing/type_incl.v
 theories/typing/perm.v
 theories/typing/typing.v
 theories/typing/lft_contexts.v
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 73ffb52bf1529122999b05e718f1c84cd34870fd..986660f763483601e464dfb79b966b29819b2e7b 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -3,7 +3,7 @@ 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 lft_contexts type_context cont_context.
+From lrust.typing Require Import typing lft_contexts type_context cont_context.
 
 Section fn.
   Context `{typeG Σ}.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index e01a07fb0e8e60c50f4ea3af9162b5302f78eda0..df8e3942d1f1bfd4ad622383e0754b48271de222 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,7 +1,7 @@
 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 perm type_incl.
+From lrust.typing Require Import perm.
 
 Section product.
   Context `{typeG Σ}.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 138f15ee16e902a68587636bbc0fdc0149309fcb..6b39fd7face0388f3621ef3ad82aacc85aa2989a 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,8 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import fractional.
 From lrust.lifetime Require Import borrow frac_borrow.
-From lrust.typing Require Export type.
-From lrust.typing Require Import type_incl.
+From lrust.typing Require Export type perm.
 
 Section sum.
   Context `{typeG Σ}.
diff --git a/theories/typing/type_incl.v b/theories/typing/type_incl.v
deleted file mode 100644
index 4cd87f378cd5dab145e1d041f271aa14c23f9948..0000000000000000000000000000000000000000
--- a/theories/typing/type_incl.v
+++ /dev/null
@@ -1,44 +0,0 @@
-From iris.base_logic Require Import big_op.
-From iris.program_logic Require Import hoare.
-From lrust.typing Require Export type perm.
-From lrust.lifetime Require Import frac_borrow borrow.
-
-Section ty_incl.
-  Context `{typeG Σ}.
-
-  Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
-    ∀ tid, lft_ctx -∗ ρ tid ={⊤}=∗
-      (□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ∗
-      (□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
-       (* [ty_incl] needs to prove something about the length of the
-          object when it is shared. We place this property under the
-          hypothesis that [ty2.(ty_shr)] holds, so that the [!] type
-          is still included in any other. *)
-                  ty2.(ty_shr) κ tid E l ∗ ⌜ty1.(ty_size) = ty2.(ty_size)⌝).
-
-  Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
-    ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ∗ θ) ty1 ty3.
-  Proof.
-    iIntros (H12 H23 tid) "#LFT [H1 H2]".
-    iMod (H12 with "LFT H1") as "[#H12 #H12']".
-    iMod (H23 with "LFT H2") as "[#H23 #H23']".
-    iModIntro; iSplit; iIntros "!#*H1".
-    - by iApply "H23"; iApply "H12".
-    - iDestruct ("H12'" $! _ _ _ with "H1") as "[H2 %]".
-      iDestruct ("H23'" $! _ _ _ with "H2") as "[$ %]".
-      iPureIntro. congruence.
-  Qed.
-
-  Lemma ty_incl_weaken ρ θ ty1 ty2 :
-    ρ ⇒ θ → ty_incl θ ty1 ty2 → ty_incl ρ ty1 ty2.
-  Proof.
-    iIntros (Hρθ Hρ' tid) "#LFT H". iApply (Hρ' with "LFT>"). iApply (Hρθ with "LFT H").
-  Qed.
-
-  Lemma ty_incl_perm_incl ρ ty1 ty2 ν :
-    ty_incl ρ ty1 ty2 → ρ ∗ ν ◁ ty1 ⇒ ν ◁ ty2.
-  Proof.
-    iIntros (Hincl tid) "#LFT [Hρ Hty1]". iMod (Hincl with "LFT Hρ") as "[#Hownincl _]".
-    unfold has_type. destruct (eval_expr ν); last done. by iApply "Hownincl".
-  Qed.
-End ty_incl.
\ No newline at end of file