Function extern_spec_T_DerefMut__refmut_T_deref_mut 

pub fn extern_spec_T_DerefMut__refmut_T_deref_mut<'a, 'b, T>(
    self_: &'b mut &'a mut T,
) -> &'b mut T

extern spec for <&mut T as DerefMut>::deref_mut

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

terminates

ghost

ensures

*result == **self

ensures

^result == *^self

ensures

^*self == ^^self