diff --git a/README.md b/README.md
index c93882d26a28df31f904563a05ea95b60826282c..e13bd896525553322f31723091841721dddd5710 100644
--- a/README.md
+++ b/README.md
@@ -71,9 +71,9 @@ The filenames are spread across `theories/typing/examples`, `theories/typing`, `
 | ------------------- | ----------------- | ------------------------ |
 | Adequacy            | `soundness.v`     | `type_soundness`         |
 | **Basic**           |                   |                          |
-| MUTBOR              | `derived_rules.v` | `ty_borrow`              |
-| MUTREF-WRITE        | `derived_rules.v` | `ty_assgn_bor_mut`       |
-| MUTREF-BYE          | `derived_rules.v` | `ty_resolve`             |
+| MUTBOR              | `derived_rules.v` | `ty_uniq_bor`            |
+| MUTREF-WRITE        | `derived_rules.v` | `ty_uniq_ref_write`      |
+| MUTREF-BYE          | `derived_rules.v` | `ty_uniq_ref_bye`        |
 | ENDLFT              | `programs.v`      | `type_endlft`            |
 | **Prophecies**      |                   |                          |
 | PROPH-INTRO         | `prophecy.v`      | `proph_intro`            |
diff --git a/theories/typing/examples/derived_rules.v b/theories/typing/examples/derived_rules.v
index e8cfab4aab74cdd7d015b34fc20927fec13014e4..90d43c06cfaef0b7a2481c881c09a494d72769b2 100644
--- a/theories/typing/examples/derived_rules.v
+++ b/theories/typing/examples/derived_rules.v
@@ -1,65 +1,61 @@
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
+Notation "drop: x" := Skip%E (only parsing, at level 102, x at level 1)
+  : expr_scope.
+
+Notation "let: x := &uniq{ κ } p 'in' e" := (let: x := p in e)%E
+  (only parsing, at level 102, x at level 1, e at level 150) : expr_scope.
+
 Section rules.
-  Local Set Warnings "-non-reversible-notation".
   Context `{!typeG Σ}.
 
-  Lemma ty_assgn_box {𝔄 𝔄'} E L p (τ : type 𝔄) p' (τ' : type 𝔄'):
-    τ.(ty_size) = τ'.(ty_size) →
-    typed_instr E L +[p ◁ box τ; p' ◁ τ'] (p <- p') (λ _, +[p ◁ box τ'])
-      (λ post '-[a; b], post -[b]).
+  Lemma ty_box_write {𝔄 𝔅} E L p (ty: type 𝔄) p' (ty': type 𝔅):
+    ty.(ty_size) = ty'.(ty_size) →
+    typed_instr E L +[p ◁ box ty; p' ◁ ty'] (p <- p') (λ _, +[p ◁ box ty'])
+      (λ post '-[_; b], post -[b]).
   Proof.
-    intros Eq ?.
-    eapply (type_assign_instr _ τ _ _ _ _ (λ _ p, p)).
-    rewrite /box Eq. solve_typing.
-    eapply resolve'_just, resolve_just.
+    move=> Eq. rewrite /box Eq.
+    eapply (type_assign_instr _ _ _ _ _ _ (λ _ post, post));
+      [solve_typing|eapply resolve'_just, resolve_just].
   Qed.
 
-  Lemma ty_assgn_bor_mut {𝔄} E L κ (τ : type 𝔄) p p' :
+  Lemma ty_uniq_ref_write {𝔄} E L κ (ty: type 𝔄) p p' :
     lctx_lft_alive E L κ →
-    typed_instr E L +[p ◁ &uniq{κ} τ; p' ◁ τ] (p <- p') (λ _, +[p ◁ &uniq{κ} τ])
-      (λ post '-[a; b], post -[(b, a.2)] ).
-  Proof.
-    intros ?.
-    eapply (type_assign_instr (&uniq{κ} τ) τ (&uniq{κ} τ) τ fst (λ v w, (w, v.2)) (λ _ p, p)).
-    solve_typing. eapply resolve'_just, resolve_just.
-  Qed.
-
-  Lemma ty_deref_bor_mut_copy {𝔄} E L κ (τ : type 𝔄) p :
-    lctx_lft_alive E L κ → Copy τ → τ.(ty_size) = 1%nat →
-    typed_instr E L +[p ◁ &uniq{κ} τ] (!p) (λ x, +[x ◁ τ; p ◁ &uniq{κ} τ])
-      (λ post '-[a], post -[a.1; a] ).
+    typed_instr E L +[p ◁ &uniq{κ} ty; p' ◁ ty] (p <- p')
+      (λ _, +[p ◁ &uniq{κ} ty]) (λ post '-[aa; b], post -[(b, aa.2)] ).
   Proof.
-    intros ???.
-    eapply type_deref_instr; [solve_typing| solve_typing].
+    move=> ?. eapply (type_assign_instr (&uniq{κ} ty) ty (&uniq{κ} ty) ty
+      fst (λ v w, (w, v.2)) (λ _ post, post)); [solve_typing|].
+    eapply resolve'_just, resolve_just.
   Qed.
 
-  Notation "drop: x" := (Skip)%E (at level 102, x at level 1) : expr_scope.
+  Lemma ty_uniq_ref_read {𝔄} E L κ (ty: type 𝔄) p :
+    lctx_lft_alive E L κ → Copy ty → ty.(ty_size) = 1%nat →
+    typed_instr E L +[p ◁ &uniq{κ} ty] (!p)
+      (λ x, +[x ◁ ty; p ◁ &uniq{κ} ty]) (λ post '-[aa], post -[aa.1; aa] ).
+  Proof. move=> ???. eapply type_deref_instr; solve_typing. Qed.
 
-  Lemma ty_resolve {𝔄} E L (τ : type 𝔄) κ p :
-  lctx_lft_alive E L κ →
-    typed_instr E L +[p ◁ &uniq{κ} τ] (drop: p) (λ _, +[])
-      (λ post '-[a], a.2 = a.1 → post -[]).
-  Proof. intros ?. eapply type_resolve_instr.
-    eapply resolve_impl. solve_typing.
-    move => [? ?] //=.
+  Lemma ty_uniq_ref_bye {𝔄} E L (ty: type 𝔄) κ p :
+    lctx_lft_alive E L κ →
+    typed_instr E L +[p ◁ &uniq{κ} ty] (drop: p) (λ _, +[])
+      (λ post '-[aa], aa.2 = aa.1 → post -[]).
+  Proof.
+    move=> ?. eapply type_resolve_instr. eapply resolve_impl; [solve_typing|].
+    by case.
   Qed.
 
-  Notation "let: x := &mut{ κ } p 'in' e" := (let: x := p in e)%E
-  (at level 102, x at level 1, e at level 150) : expr_scope.
-
-  Lemma ty_borrow {𝔄 𝔄l ℭ} E L (C : cctx ℭ) (T : tctx 𝔄l) (τ : type 𝔄) p x e κ tr:
-    Closed (x :b: []) e → elctx_sat E L (ty_outlives_E τ κ) →
-    (∀v: val, typed_body E L C (v ◁ &uniq{κ} τ +:: p ◁{κ} box τ +:: T) (subst' x v e) tr) -∗
-    typed_body E L C (p ◁ box τ +:: T) (let: x := &mut{κ} p in e)
-      (λ post '(a -:: t), (∀ a', tr post ((a, a') -:: a' -:: t)) : Prop).
+  Lemma ty_uniq_bor {𝔄 𝔄l ℭ} E L (C: cctx ℭ) (T: tctx 𝔄l) (ty: type 𝔄) p x e κ tr:
+    Closed (x :b: []) e → elctx_sat E L (ty_outlives_E ty κ) →
+    (∀v: val, typed_body E L C
+      (v ◁ &uniq{κ} ty +:: p ◁{κ} box ty +:: T) (subst' x v e) tr) -∗
+    typed_body E L C (p ◁ box ty +:: T) (let: x := &uniq{κ} p in e)
+      (λ post '(a -:: t), (∀ a', tr post ((a, a') -:: a' -:: t)))%type.
   Proof.
-    iIntros (??) "H". via_tr_impl.
-    iApply typed_body_tctx_incl.
-    eapply (tctx_incl_app +[_] +[_; _] T T _ id), tctx_incl_refl.
-    eapply tctx_borrow; [done].
-    iApply (type_let' +[_]); [eapply type_path_instr| done].
-    rewrite /trans_app => ? [? ?] //=.
+    iIntros (??) "?". via_tr_impl.
+    { iApply typed_body_tctx_incl.
+      { eapply (tctx_incl_frame_r +[_]). by eapply tctx_borrow. }
+      iApply type_letpath; [solve_typing|done]. }
+    by move=> ?[??].
   Qed.
 End rules.
\ No newline at end of file