Function btree_set_remove_ensures 

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

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

    })
        ==> {
            &&& btree_set_inv(final_m)
            &&& if result {
                exists |key: Key| {
                    &&& #[trigger] old_m@.contains(key)
                    &&& k.cmp_spec(<Key as BorrowSpec<Q>>::borrow_spec(&key)) is Equal
                    &&& final_m@ == old_m@.remove(key)

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

            }

        }
}