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),m1.submap_of(m3),submap_of (<=) is transitive.