Skip to main content

lemma_submap_of_trans

vstd::imap_lib

Function lemma_submap_of_trans 

Source 
pub broadcast proof fn lemma_submap_of_trans<K, V>(
    m1: IMap<K, V>,
    m2: IMap<K, V>,
    m3: IMap<K, V>,
)
Expand description
requires
#[trigger] m1.submap_of(m2),
#[trigger] m2.submap_of(m3),
ensures
m1.submap_of(m3),

submap_of (<=) is transitive.