One important thing to note is that an &'a mut T<'b> can be converted to an exists<'c> &'a mut T<'c>, but it can't soundly be converted to an &'a mut exists<'c> T<'c>. The former type allows changing the value but requires the lifetime to be the same, whereas the latter type allows changing both the value and the lifetime. The latter type is still sound as long as it was obtained by actually taking a reference to an exists<'c> T<'c> - overwriting the lifetime is fine at that point, cause nobo...
