RefMut can be considered as Sync

(Even though Rust stdlib does not consider it as such.)

theories/typing/lib/refcell/refmut.v

@@ -123,6 +123,10 @@ Section refmut.
     lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
     eqtype E L (refmut α1 ty1) (refmut α2 ty2).
   Proof. intros. by eapply refmut_proper. Qed.
+
+  Global Instance refmut_sync α ty :
+    Sync ty → Sync (refmut α ty).
+  Proof. move=>?????/=. do 10 f_equiv. by rewrite sync_change_tid. Qed.
 End refmut.
 
 Global Hint Resolve refmut_mono' refmut_proper' : lrust_typing.