Function fresh_frame_id Copy item path

pub open spec fn fresh_frame_id(m: Map<FrameId, FrameEntry>) -> FrameId

{ choose |id: FrameId| !m.dom().contains(id) }