Function extern_spec_T_U_AsMut_U__refmut_T_as_mut 

pub fn extern_spec_T_U_AsMut_U__refmut_T_as_mut<'a, 'b, T, U: ?Sized>(
    self_: &'b mut &'a mut T,
) -> &'b mut U
where
    T: AsMut<U> + ?Sized,

extern spec for <&mut T as AsMut<U>>::as_mut

This is not a real function: its only use is for documentation.

requires

<T as AsMut<U>>::as_mut.precondition((*self,))

ensures

self == ^^self

ensures

self && ^s == *^self