diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index cd9a14092086698e8f3fa178379b399e118d2876..73140880af6b19204077569b6c8d37504dc8814a 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -10,15 +10,6 @@ Set Default Proof Using "Type".
 
 Definition mutexN := lrustN .@ "mutex".
 
-(* This type is an experiment in defining a Rust type on top of a non-typesysten-specific
-   interface, like the one provided by lang.lib.lock.
-   It turns out that we need an accessor-based spec for this purpose, so that
-   we can put the protocol into shared borrows.  Cancellable invariants
-   don't work because their cancelling view shift has a non-empty mask,
-   and it would have to be executed in the consequence view shift of
-   a borrow.
-*)
-
 Section mutex.
   Context `{!typeG Σ, !lockG Σ}.
 
@@ -99,6 +90,26 @@ Section mutex.
     constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
   Qed.
 
+  Global Instance mutex_mono E L : Proper (eqtype E L ==> subtype E L) mutex.
+  Proof.
+    move=>ty1 ty2 /eqtype_unfold EQ. iIntros (?) "HL".
+    iDestruct (EQ with "HL") as "#EQ". iIntros "!# #HE". clear EQ.
+    iDestruct ("EQ" with "HE") as "(% & #Howni & _) {EQ}".
+    iSplit; last iSplit.
+    - simpl. iPureIntro. f_equiv. done.
+    - iIntros "!# * Hvl". destruct vl as [|[[| |n]|]vl]; try done.
+      simpl. iDestruct "Hvl" as "[$ Hvl]". by iApply "Howni".
+    - iIntros "!# * Hshr". iDestruct "Hshr" as (γ κ') "[Hshr Hincl]".
+      iExists _, _. iFrame "Hincl". iApply (shr_bor_iff with "[] Hshr"). iNext.
+      iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
+      iApply heap_mapsto_pred_iff_proper.
+      iAlways; iIntros; iSplit; iIntros; by iApply "Howni".
+  Qed.
+
+  Global Instance mutex_proper E L :
+    Proper (eqtype E L ==> eqtype E L) mutex.
+  Proof. by split; apply mutex_mono. Qed.
+
   Global Instance mutex_send ty :
     Send ty → Send (mutex ty).
   Proof.
@@ -116,8 +127,6 @@ Section mutex.
     iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
   Qed.
 
-  (* TODO: compat with eqtype. *)
-
 End mutex.
 
 Section code.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index d3f1762e1201894be4ea3e10b81926d3f9327f8a..17ac49c009731a5cc1d2a559a7ab635f641fa42c 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -88,7 +88,38 @@ Section mguard.
   Global Instance mutexguard_ne α : NonExpansive (mutexguard α).
   Proof. apply type_contractive_ne, _. Qed.
 
-  (* TODO: compat with lft_incl and eqtype. *)
+  Global Instance mutexguard_mono E L :
+    Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) mutexguard.
+  Proof.
+    intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold. iIntros (Hty' q) "HL".
+    iDestruct (Hty' with "HL") as "#Hty". clear Hty'. iDestruct (Hα with "HL") as "#Hα".
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "{Hα} Hα".
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iAlways].
+    - iIntros (tid [|[[]|][]]) "H"; try done. simpl.
+      iDestruct "H" as (γ β) "(Hcl & #H⊑ & #Hinv & Hown)".
+      iExists γ, β. iFrame. iSplit; last iSplit.
+      + by iApply lft_incl_trans.
+      + iApply (shr_bor_shorten with "Hα").
+        iApply (shr_bor_iff with "[] Hinv"). iNext.
+        iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
+        iApply heap_mapsto_pred_iff_proper.
+        iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
+      + iApply bor_iff; last done. iNext.
+        iApply heap_mapsto_pred_iff_proper.
+        iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
+    - iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
+      iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+      { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
+      iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+      iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+      iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+      by iApply "Hs".
+  Qed.
+
+  Global Instance mutexguard_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E  L) mutexguard.
+  Proof. intros ??[]???. split; by apply mutexguard_mono. Qed.
 
   Global Instance mutexguard_sync α ty :
     Sync ty → Sync (mutexguard α ty).