diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index da77afe2a4ec222e5fe061e039578432c0cab97c..74c6b1c953f5f20646e5909da8b70e90efd55079 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -27,7 +27,7 @@ Section proof.
 
   Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
 
-  Global Instance lock_inv_ne γ l : NonExpansive (lock_proto γ l).
+  Global Instance lock_proto_ne γ l : NonExpansive (lock_proto γ l).
   Proof. solve_proper. Qed.
 
   Global Instance locked_timeless γ : TimelessP (locked γ).
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index f6c4e3593237737d03e61a30f537b93ca314a6cb..8d83630d44cd77544bbf2b043eae828ced9d9ca5 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -87,7 +87,19 @@ Section mutex.
   Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
     { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
 
-  (* TODO: Non-expansiveness, compat with eqtype, Send+Sync if ty is Send. *)
+  Global Instance mutex_type_ne : TypeNonExpansive mutex.
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance mutex_ne : NonExpansive mutex.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
+  (* TODO: compat with eqtype, Send+Sync if ty is Send. *)
 
 End mutex.
 
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 0a04209e0199d5a50c3cf04055ff9ae21f457e27..66a94e0da26cd239cc151f782597323caccaacfa 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -79,7 +79,16 @@ Section mguard.
   Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
     { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
 
-  (* TODO: Contractivity, compat with lft_incl and eqtype.
+  Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv
+                                    || exact: type_dist2_S).
+  Qed.
+  Global Instance mutexguard_ne α : NonExpansive (mutexguard α).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  (* TODO: compat with lft_incl and eqtype.
      MutexGuard is Sync if T is Send. *)
 
 End mguard.