diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 321a07895aad959861d3f0db3c2ea7e2d8650412..328133abd8bab0bb93f1c056156a17e98f05db2d 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -23,6 +23,8 @@ Section proof.
 
   Global Instance lock_proto_ne l : NonExpansive (lock_proto l).
   Proof. solve_proper. Qed.
+  Global Instance lock_proto_proper l : Proper ((≡) ==> (≡)) (lock_proto l).
+  Proof. apply ne_proper, _. Qed.
 
   Lemma lock_proto_iff l R R' :
     □ (R ↔ R') -∗ lock_proto l R -∗ lock_proto l R'.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 25fbede9afb92d6c7b3d4f586dea638e8efee81a..11b48b8f1960f6cab9a7bf87a6d9e7016ec6f5b5 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -125,8 +125,18 @@ Section mguard.
   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. *)
+     the lock, so Rust does not implement Send for MutexGuard. We can
+     prove this for our spinlock implementation, however. *)
+  Global Instance mutexguard_send α ty :
+    Send ty → Send (mutexguard α ty).
+  Proof.
+    iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
+    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+    repeat match goal with
+           | |- (ty_own _ _ _) ≡ (ty_own _ _ _) => by apply send_change_tid'
+           | |- _ => f_equiv
+           end.
+  Qed.
 End mguard.
 
 Section code.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 04f19c8e4782b830713a42044cd6503bcc9bf1be..38434666bb01294d2d24342cbee412c038c0c522 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -80,6 +80,16 @@ Section rwlock_inv.
     iFrame. iSplitR. done. iSplitL "Hh"; last by iApply "Hshr".
     iIntros "Hν". iApply "Hb". iApply ("Hh" with "Hν").
   Qed.
+
+  Lemma rwlock_inv_change_tid tid1 tid2 l γ α ty :
+    Send ty → Sync ty →
+    rwlock_inv tid1 l γ α ty ≡ rwlock_inv tid2 l γ α ty.
+  Proof.
+    intros ??. apply bi.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
+    - do 5 f_equiv. iApply send_change_tid'.
+    - iApply sync_change_tid'.
+    - iApply send_change_tid'.
+  Qed.
 End rwlock_inv.
 
 Section rwlock.
@@ -200,11 +210,7 @@ Section rwlock.
     Send ty → Sync ty → Sync (rwlock ty).
   Proof.
     move=>??????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
-    iApply at_bor_iff. iIntros "!> !#". iApply bi.equiv_iff.
-    apply bi.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
-    - do 5 f_equiv. apply bi.equiv_spec; split; iApply send_change_tid.
-    - apply bi.equiv_spec; split; iApply sync_change_tid.
-    - apply bi.equiv_spec; split; iApply send_change_tid.
+    apply bi.equiv_spec. f_equiv. apply: rwlock_inv_change_tid.
   Qed.
 End rwlock.
 
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 9dd3999a079898955ced24d72fe84074cb815315..35b4be01fa837db8c23199e2a31e7a83fe853474 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -121,8 +121,19 @@ Section rwlockreadguard.
   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. *)
+     the lock, so Rust does not implement Send for RwLockWriteGuard. We can
+     prove this for our spinlock implementation, however. *)
+  Global Instance rwlockreadguard_send α ty :
+    Send ty → Sync ty → Send (rwlockreadguard α ty).
+  Proof.
+    iIntros (???? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
+    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+    repeat lazymatch goal with
+           | |- (ty_shr _ _ _ _) ≡ (ty_shr _ _ _ _) => by apply sync_change_tid'
+           | |- (rwlock_inv _ _ _ _ _) ≡ _ => by apply rwlock_inv_change_tid
+           | |- _ => f_equiv
+           end.
+  Qed.
 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 7b8576d5ca62f9a0bae082df5be29d4d375183a6..80a197ecdc992d0dc47fdda1a030c24cfbde621c 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -125,8 +125,19 @@ Section rwlockwriteguard.
   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. *)
+     the lock, so Rust does not implement Send for RwLockWriteGuard. We can
+     prove this for our spinlock implementation, however. *)
+  Global Instance rwlockwriteguard_send α ty :
+    Send ty → Sync ty → Send (rwlockwriteguard α ty).
+  Proof.
+    iIntros (???? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
+    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+    repeat lazymatch goal with
+           | |- (ty_own _ _ _) ≡ (ty_own _ _ _) => by apply send_change_tid'
+           | |- (rwlock_inv _ _ _ _ _) ≡ _ => by apply rwlock_inv_change_tid
+           | |- _ => f_equiv
+           end.
+  Qed.
 End rwlockwriteguard.
 
 Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index bcc034cbf9444c81c6543d1ed3cd45c9af09de1e..b090940de3318eb50d539bb0b3eecd412c61cf17 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -519,6 +519,18 @@ Section type.
     iIntros (Hsend κ tid1 tid2 l). iDestruct 1 as (vl) "[Hm Hown]".
     iExists vl. iFrame "Hm". iNext. by iApply Hsend.
   Qed.
+
+  Lemma send_change_tid' t tid1 tid2 vl :
+    Send t → t.(ty_own) tid1 vl ≡ t.(ty_own) tid2 vl.
+  Proof.
+    intros ?. apply: anti_symm; apply send_change_tid.
+  Qed.
+
+  Lemma sync_change_tid' t κ tid1 tid2 l :
+    Sync t → t.(ty_shr) κ tid1 l ≡ t.(ty_shr) κ tid2 l.
+  Proof.
+    intros ?. apply: anti_symm; apply sync_change_tid.
+  Qed.
 End type.
 
 Definition type_incl `{!typeG Σ} (ty1 ty2 : type) : iProp Σ :=