diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index a150166d10efd01b75d088fb3656ce7456324988..d3f1762e1201894be4ea3e10b81926d3f9327f8a 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -88,9 +88,18 @@ Section mguard.
   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. *)
+  (* TODO: compat with lft_incl and eqtype. *)
 
+  Global Instance mutexguard_sync α ty :
+    Sync ty → Sync (mutexguard α ty).
+  Proof.
+    move=>?????/=. apply uPred.exist_mono=>?. do 6 f_equiv.
+    by rewrite sync_change_tid.
+  Qed.
+
+  (* POSIX requires the unlock to occur from the thread that acquired
+     the lock, so Rust does not implement Send for RwLockWriteGuard. We could
+     prove this. *)
 End mguard.
 
 Section code.