Function btree_map_contains_key_ensures 

pub open spec fn btree_map_contains_key_ensures<Key: Borrow<Q> + Ord, Value, A: Allocator + Clone, Q: Ord + ?Sized>(
    m: &BTreeMap<Key, Value, A>,
    k: &Q,
    result: bool,
) -> bool

{
    ({
        &&& obeys_cmp::<Key>()
        &&& obeys_cmp::<&Q>()
        &&& <Key as BorrowSpec<Q>>::obeys_borrow_spec()
        &&& btree_map_inv(m)

    })
        ==> {
            &&& result
                == exists |key: Key| {
                    &&& #[trigger] m@.contains_key(key)
                    &&& k.cmp_spec(<Key as BorrowSpec<Q>>::borrow_spec(&key)) is Equal

                }

        }
}