Function arbitrary_cell_pointsto Copy item path

pub proof fn arbitrary_cell_pointsto<T>() -> tracked res : PointsTo<T>