Function box_deref_spec Copy item path

pub broadcast proof fn box_deref_spec<T>(b: Box<T>)

#[trigger] *(b.deref_spec()) == *b,