Map extensional equality sensitive to order

[jaylorch]

Map extensional equality is sensitive to the order of the arguments to =~=. For instance, this code doesn't work unless you put the arguments in a particular order:

proof fn test_map_extensional_equality_fails(m1: Map<int, int>, m2: Map<int, int>)
    requires
        forall|i: int| #![trigger m2.contains_key(i)]
            if m2.contains_key(i) { m1.contains_key(i) && m1[i] == m2[i] } else { !m1.contains_key(i) },
    ensures
        m1 == m2,
{
    assert(m1 =~= m2); // doesn't work
//    assert(m2 =~= m1); // they need to be in this order
}