Function lemma_fresh_segment_id_not_in_dom Copy item path

pub proof fn lemma_fresh_segment_id_not_in_dom(m: Map<SegmentId, SegmentEntry>)

!m.dom().contains(fresh_segment_id(m)),