diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 1030c87273c87574b8c250bd686e437155b04f78..23fb26f041e561e56d9fd785551f4a09260c58c2 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -83,4 +83,8 @@ Section mutex.
     iExists _, _. iSplit; first by iApply shr_bor_shorten.
     iApply lft_incl_trans; done.
   Qed.
+
+  Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
 End mutex.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index d9c1556836b73e448e1795d680697c2110a96355..034ed18c3972978e23effa6e0ab8ac2d51623fed 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -75,4 +75,8 @@ Section mguard.
       iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
       iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
   Qed.
+
+  Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
 End mguard.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index db17b3e5830be1ea7c2944aa7cf6055eda0c95d5..a75c30b74c9169d2ee33bcb6955d4539396e96d0 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -149,7 +149,7 @@ Section rwlock.
     iExists _, _. iFrame. iApply lft_incl_trans; auto.
   Qed.
 
-  Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
+  Global Instance rwlock_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
     { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
 
   Global Instance rwlock_type_ne : TypeNonExpansive rwlock.