ref_deref_spec

vstd_extra::external::deref

Function ref_deref_spec 

Source 
pub broadcast proof fn ref_deref_spec<T>(r: &T)
Expand description
ensures
#[trigger] *(r.deref_spec()) == *r,