Function axiom_unpack_mut_ref_current 

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

ensures

mut_ref_current(a) == (#[trigger] MutRef::unpack(a)).current,