Function vstd::map_lib::lemma_submap_of_trans

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

submap_of (<=) is transitive.