pub trait ForLoopGhostIteratorNew { type GhostIter; // Required method spec fn ghost_iter(&self) -> Self::GhostIter; }