Function extern_spec_T_Deref__ref_T_deref 

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

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

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

terminates

ghost

ensures

*result == **self