Function btree_map_get_mut_ensures 

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

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

    })
        ==> {
            &&& btree_map_inv(final_m)
            &&& match result {
                Some((current_value, final_value)) => {
                    exists |stored_key: Key| {
                        &&& #[trigger] old_m@.contains_key(stored_key)
                        &&& k
                            .cmp_spec(
                                <Key as BorrowSpec<Q>>::borrow_spec(&stored_key),
                            ) is Equal
                        &&& old_m@[stored_key] == current_value
                        &&& final_m@ == old_m@.insert(stored_key, final_value)

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

                ),
            }

        }
}