Function btree_map_inv 

pub open spec fn btree_map_inv<Key: Ord, Value, A: Allocator + Clone>(
    m: &BTreeMap<Key, Value, A>,
) -> bool

{
    forall |k1: Key, k2: Key| (
        {
            &&& #[trigger] m@.contains_key(k1)
            &&& #[trigger] m@.contains_key(k2)
            &&& k1 != k2

        } ==> !(k1.cmp_spec(&k2) is Equal)
    )
}