Skip to main content

lemma_fresh_segment_id_not_in_dom

ostd::specs::mm::embedding

Function lemma_fresh_segment_id_not_in_dom 

Source 
pub proof fn lemma_fresh_segment_id_not_in_dom(m: Map<SegmentId, SegmentEntry>)
Expand description
ensures
!m.contains_key(fresh_segment_id(m)),