Function extern_spec_T_Deref__refmut_T_deref 

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

extern spec for <&mut T as Deref>::deref

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

terminates

ghost

ensures

*result == **self