diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index a5c20914cd56a442978e2a6953cf08f3f95ad102..f6c4e3593237737d03e61a30f537b93ca314a6cb 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -87,6 +87,8 @@ 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. *)
+
 End mutex.
 
 Section code.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index d602d839f193fc64585ea3bc16fd224d8c8fb8b5..0a04209e0199d5a50c3cf04055ff9ae21f457e27 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -79,6 +79,9 @@ 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.
+     MutexGuard is Sync if T is Send. *)
+
 End mguard.
 
 Section code.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 3f44a88e8d599be379c2eae4b57633218ad58169..e21b832db4572cca59bddef14991fea16e7d788e 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -112,6 +112,8 @@ Section rwlockreadguard.
     lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
     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. *)
 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 9da6cf5008effcd6916818affd5c5eafddf605b3..400022088ee7966bcb1b2c3af170eb8f8a20020f 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -115,6 +115,8 @@ Section rwlockwriteguard.
     lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
     eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2).
   Proof. intros. by eapply rwlockwriteguard_proper. Qed.
+
+  (* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *)
 End rwlockwriteguard.
 
 Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.