RefMut can be considered as Sync

I figured out that RefMut could be considered as Sync even though Rust stdlib does not consider it as such.

I find this is an interesting fact, so I added it to our formalization. This is not particularly useful for writing programs, because a value of type &RefMut<T> can be WLOG unnested to a &T, but still this is interesting from a type system's perspective.

Yes, this is an interesting fact indeed, thanks! Can you add a comment saying that this instance does not exist in actual Rust but we prove it anyway?