Function lemma_fresh_frame_id_not_in_dom 

pub proof fn lemma_fresh_frame_id_not_in_dom(m: Map<FrameId, FrameEntry>)

ensures

!m.contains_key(fresh_frame_id(m)),