Function btree_set_get_ensures 

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

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

    })
        ==> {
            &&& match result {
                Some(key) => (
                    &&& m@.contains(*key)
                    &&& k.cmp_spec(<Key as BorrowSpec<Q>>::borrow_spec(key)) is Equal

                ),
                None => {
                    forall |key: Key| (
                        #[trigger] m@.contains(key)
                            ==> !(k
                                .cmp_spec(
                                    <Key as BorrowSpec<Q>>::borrow_spec(&key),
                                ) is Equal)
                    )
                }
            }

        }
}