diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index 1189e4b845b67bf739c4ab47eb53b87c7250d8b8..a09cc07bd93656b1d99aa8965cef38ef501273c9 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -106,75 +106,3 @@ Section has_type.
       iApply ("IH" with "[] [HΦ]"). done. simpl. wp_op. inversion EQν. eauto.
   Qed.
 End has_type.
-(*
-Section perm_incl.
-  Context `{typeG Σ}.
-
-  (* Properties *)
-  Global Instance perm_incl_preorder : PreOrder (⇒).
-  Proof.
-    split.
-    - iIntros (? tid) "H". eauto.
-    - iIntros (??? H12 H23 tid) "#LFT H". iApply (H23 with "LFT >").
-      by iApply (H12 with "LFT").
-  Qed.
-
-  Global Instance perm_equiv_equiv : Equivalence (⇔).
-  Proof.
-    split.
-    - by split.
-    - by intros x y []; split.
-    - intros x y z [] []. split; by transitivity y.
-  Qed.
-
-  Global Instance perm_incl_proper :
-    Proper ((⇔) ==> (⇔) ==> iff) (⇒).
-  Proof. intros ??[??]??[??]; split; intros ?; by simplify_order. Qed.
-
-  Global Instance perm_sep_proper :
-    Proper ((⇔) ==> (⇔) ==> (⇔)) (sep).
-  Proof.
-    intros ??[A B]??[C D]; split; iIntros (tid) "#LFT [A B]".
-    iMod (A with "LFT A") as "$". iApply (C with "LFT B").
-    iMod (B with "LFT A") as "$". iApply (D with "LFT B").
-  Qed.
-
-  Lemma uPred_equiv_perm_equiv ρ θ : (∀ tid, ρ tid ⊣⊢ θ tid) → (ρ ⇔ θ).
-  Proof. intros Heq. split=>tid; rewrite Heq; by iIntros. Qed.
-
-  Lemma perm_incl_top ρ : ρ ⇒ ⊤.
-  Proof. iIntros (tid) "H". eauto. Qed.
-
-  Lemma perm_incl_frame_l ρ ρ1 ρ2 : ρ1 ⇒ ρ2 → ρ ∗ ρ1 ⇒ ρ ∗ ρ2.
-  Proof. iIntros (Hρ tid) "#LFT [$?]". by iApply (Hρ with "LFT"). Qed.
-
-  Lemma perm_incl_frame_r ρ ρ1 ρ2 :
-    ρ1 ⇒ ρ2 → ρ1 ∗ ρ ⇒ ρ2 ∗ ρ.
-  Proof. iIntros (Hρ tid) "#LFT [?$]". by iApply (Hρ with "LFT"). Qed.
-
-  Lemma perm_incl_exists_intro {A} P x : P x ⇒ ∃ x : A, P x.
-  Proof. iIntros (tid) "_ H!>". by iExists x. Qed.
-
-  Global Instance perm_sep_assoc : Assoc (⇔) sep.
-  Proof. intros ???; split. by iIntros (tid) "_ [$[$$]]". by iIntros (tid) "_ [[$$]$]". Qed.
-
-  Global Instance perm_sep_comm : Comm (⇔) sep.
-  Proof. intros ??; split; by iIntros (tid) "_ [$$]". Qed.
-
-  Global Instance perm_top_right_id : RightId (⇔) ⊤ sep.
-  Proof. intros ρ; split. by iIntros (tid) "_ [? _]". by iIntros (tid) "_ $". Qed.
-
-  Global Instance perm_top_left_id : LeftId (⇔) ⊤ sep.
-  Proof. intros ρ. by rewrite comm right_id. Qed.
-
-  Lemma perm_tok_plus κ q1 q2 :
-    tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
-  Proof. rewrite /tok /sep /=; split; by iIntros (tid) "_ [$$]". Qed.
-
-  Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
-  Proof. iIntros (tid) "_ _!>". iApply lft_incl_refl. Qed.
-
-  Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
-  Proof. iIntros (tid) "_ [#?#?]!>". iApply (lft_incl_trans with "[] []"); auto. Qed.
-End perm_incl.
-*)
\ No newline at end of file
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index a9f97dd81fc9c4247b316f37e75c178cc6fc3408..27feaf7dd2a07dc571a6db89325623eb5622cb3b 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -22,26 +22,6 @@ Section typing.
   Definition typed_program (ρ : perm) e :=
     ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ na_own tid ⊤ }} e {{ _, False }}.
 
-  Lemma typed_frame ρ e θ ξ:
-    typed_step ρ e θ → typed_step (ρ ∗ ξ) e (λ ν, θ ν ∗ ξ)%P.
-  Proof.
-    iIntros (Hwt tid) "!#(#HEAP&#LFT&[?$]&?)". iApply Hwt. iFrame "∗#".
-  Qed.
-
-  Lemma typed_step_exists {A} ρ θ e ξ:
-    (∀ x:A, typed_step (ρ ∗ θ x) e ξ) →
-    typed_step (ρ ∗ ∃ x, θ x) e ξ.
-  Proof.
-    iIntros (Hwt tid) "!#(#HEAP&#LFT&[Hρ Hθ]&?)". iDestruct "Hθ" as (x) "Hθ".
-    iApply Hwt. iFrame "∗#".
-  Qed.
-
-  Lemma typed_valuable (ν : expr) ty:
-    typed_step_ty (ν ◁ ty) ν ty.
-  Proof.
-    iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "_ $".
-  Qed.
-
   Lemma typed_newlft ρ:
     typed_step ρ Newlft (λ _, ∃ α, 1.[α] ∗ α ∋ top)%P.
   Proof.
@@ -68,17 +48,6 @@ Section typing.
        -∗ Φ #l)
       -∗ WP ν @ E {{ Φ }}.
 
-  Lemma typed_deref ty ρ1 ρ2 (ν:expr) :
-    ty.(ty_size) = 1%nat → consumes ty ρ1 ρ2 →
-    typed_step (ρ1 ν) (!ν) (λ v, v ◁ ty ∗ ρ2 ν)%P.
-  Proof.
-    iIntros (Hsz Hconsumes tid) "!#(#HEAP & #LFT & Hρ1 & Htl)". wp_bind ν.
-    iApply (Hconsumes with "LFT Hρ1 Htl"). done. iFrame. iIntros (l vl q) "(%&%&H↦&>Hupd)".
-    rewrite ->Hsz in *. destruct vl as [|v [|]]; try done.
-    rewrite heap_mapsto_vec_singleton. wp_read. rewrite /sep has_type_value.
-    iMod "Hupd" as "[$ Hclose]". by iApply "Hclose".
-  Qed.
-
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
     ∀ ν tid Φ E, lftE ∪ (↑lrustN) ⊆ E →
       lft_ctx -∗ ρ1 ν tid -∗
@@ -87,54 +56,4 @@ Section typing.
            ∀ vl', l ↦∗ vl' ∗ ▷ (ty.(ty_own) tid vl') ={E}=∗ ρ2 ν tid) -∗ Φ #l) -∗
       WP ν @ E {{ Φ }}.
 
-  Lemma typed_assign ρ1 ρ2 ty ν1 ν2:
-    ty.(ty_size) = 1%nat → update ty ρ1 ρ2 →
-    typed_step (ρ1 ν1 ∗ ν2 ◁ ty) (ν1 <- ν2) (λ _, ρ2 ν1).
-  Proof.
-    iIntros (Hsz Hupd tid) "!#(#HEAP & #LFT & [Hρ1 H◁] & $)". wp_bind ν1.
-    iApply (Hupd with "LFT Hρ1"). done. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
-    rewrite ->Hsz in *. destruct vl as [|v[|]]; try done.
-    wp_bind ν2. iApply (has_type_wp with "H◁"). iIntros (v') "% H◁!>".
-    rewrite heap_mapsto_vec_singleton. wp_write.
-    rewrite -heap_mapsto_vec_singleton has_type_value. iApply "Hupd". by iFrame.
-  Qed.
-
-  Lemma typed_memcpy ρ1 ρ1' ρ2 ρ2' ty ν1 ν2:
-    update ty ρ1' ρ1 → consumes ty ρ2' ρ2 →
-    typed_step (ρ1' ν1 ∗ ρ2' ν2) (ν1 <-{ty.(ty_size)} !ν2) (λ _, ρ1 ν1 ∗ ρ2 ν2)%P.
-  Proof.
-    iIntros (Hupd Hcons tid) "!#(#HEAP & #LFT & [H1 H2] & Htl)". wp_bind ν1.
-    iApply (Hupd with "LFT H1"). done.
-    iIntros (l vl) "(% & % & H↦ & Hupd)". wp_bind ν2.
-    iApply (Hcons with "LFT H2 Htl"). done.
-    iIntros (l' vl' q) "(% & % & H↦' & Hcons)". iApply wp_fupd.
-    iMod "Hcons". iApply (wp_memcpy with "[$HEAP $H↦' $H↦]"); try done. iNext.
-    iIntros "[H↦ H↦']". iMod "Hcons" as "[Hown' Hcons]".
-    iMod ("Hcons" with "H↦'") as "[$$]". iApply "Hupd". by iFrame.
-  Qed.
-(*
-  Lemma typed_weaken ρ1 ρ2 e:
-    typed_program ρ2 e → (ρ1 ⇒ ρ2) → typed_program ρ1 e.
-  Proof.
-    iIntros (Hρ2 Hρ12 tid) "!#(#HEAP & #LFT & Hρ1 & Htl)".
-    iApply (Hρ2 with ">"). iFrame "∗#". iApply (Hρ12 with "LFT Hρ1").
-  Qed.
-*)
-  Lemma typed_program_exists {A} ρ θ e:
-    (∀ x:A, typed_program (ρ ∗ θ x) e) →
-    typed_program (ρ ∗ ∃ x, θ x) e.
-  Proof.
-    iIntros (Hwt tid) "!#(#HEAP & #LFT & [Hρ Hθ] & ?)". iDestruct "Hθ" as (x) "Hθ".
-    iApply Hwt. iFrame "∗#".
-  Qed.
-
-  Lemma typed_step_program ρ θ e K:
-    typed_step ρ e θ →
-    (∀ v, typed_program (θ v) (fill K (of_val v))) →
-    typed_program ρ (fill K e).
-  Proof.
-    iIntros (He HK tid) "!#(#HEAP & #LFT & Hρ & Htl)".
-    iApply wp_bind. iApply wp_wand_r. iSplitL. iApply He; iFrame "∗#".
-    iIntros (v) "[Hθ Htl]". iApply HK. iFrame "∗#".
-  Qed.
 End typing.