Function fresh_unique_id Copy item path

pub open spec fn fresh_unique_id(m: Map<UniqueId, UniqueEntry>) -> UniqueId

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