Function fresh_loose_id Copy item path

pub open spec fn fresh_loose_id<M: AnyFrameMeta + Repr<MetaSlotSmall>>(
    m: Map<LooseId, UniqueFrameOwner<Link<M>>>,
) -> LooseId

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