Function vstd::map::axiom_map_ext_equal_deep

source · 
pub broadcast proof fn axiom_map_ext_equal_deep<K, V>(m1: Map<K, V>, m2: Map<K, V>)
Expand description
ensures
#[trigger] (m1 =~~= m2)
    <==> {
        &&& m1.dom() =~~= m2.dom()
        &&& forall |k: K| m1.dom().contains(k) ==> m1[k] =~~= m2[k]

    },