Function vstd::map::axiom_map_ext_equal

pub broadcast proof fn axiom_map_ext_equal<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]

    },

Two maps are equivalent if their domains are equivalent and every key in their domains map to the same value.