Function axiom_unpack_mut_ref_future 

pub broadcast proof fn axiom_unpack_mut_ref_future<T>(a: &mut T)

ensures

mut_ref_future(a) == (#[trigger] MutRef::unpack(a)).future.value(),