Function fresh_frame_id 

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

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

Picks a FrameId not currently in m.dom().