Function lemma_segment_cover_witness 

pub proof fn lemma_segment_cover_witness(
    segments: Map<SegmentId, SegmentEntry>,
    paddr: Paddr,
) -> sid : SegmentId

requires

segment_cover_count(segments, paddr) > 0,

ensures

segments.contains_key(sid),

segments[sid].range.start <= paddr < segments[sid].range.end,

A positive segment-cover count exhibits a witnessing segment id whose range covers paddr.