diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index e21b832db4572cca59bddef14991fea16e7d788e..64ae740d5d6c08cb471aea913747e563423d5d79 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -113,7 +113,15 @@ Section rwlockreadguard.
     eqtype E L (rwlockreadguard α1 ty1) (rwlockreadguard α2 ty2).
   Proof. intros. by eapply rwlockreadguard_proper. Qed.
 
-  (* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *)
+  Global Instance rwlockreadguard_sync α ty :
+    Sync ty → Sync (rwlockreadguard α ty).
+  Proof.
+    move=>?????/=. apply uPred.exist_mono=>?. by rewrite sync_change_tid.
+  Qed.
+
+  (* Probably for reasons related to the underlying representation,
+     Rust does not implement Send for RwLockWriteGuard. We could prove
+     this. *)
 End rwlockreadguard.
 
 Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 985ed87d42590bd44f17182cc64fed589e64b2d4..b439613c138162fa8879b04525246a3078f079a0 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -116,7 +116,16 @@ Section rwlockwriteguard.
     eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2).
   Proof. intros. by eapply rwlockwriteguard_proper. Qed.
 
-  (* TODO: In Rust, the write guard is Sync if ty is Send+Sync. *)
+  Global Instance rwlockwriteguard_sync α ty :
+    Sync ty → Sync (rwlockwriteguard α ty).
+  Proof.
+    move=>?????/=. apply uPred.exist_mono=>?. do 6 f_equiv.
+    by rewrite sync_change_tid.
+  Qed.
+
+  (* Probably for reasons related to the underlying representation,
+     Rust does not implement Send for RwLockWriteGuard. We could prove
+     this. *)
 End rwlockwriteguard.
 
 Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.