Function btree_map_insert_ensures 

pub open spec fn btree_map_insert_ensures<Key: Ord, Value, A: Allocator + Clone>(
    old_m: &BTreeMap<Key, Value, A>,
    final_m: &BTreeMap<Key, Value, A>,
    k: Key,
    v: Value,
    result: Option<Value>,
) -> bool

{
    obeys_cmp::<Key>() && btree_map_inv(old_m)
        ==> {
            &&& btree_map_inv(final_m)
            &&& match result {
                Some(old_value) => {
                    exists |stored_key: Key| {
                        &&& #[trigger] old_m@.contains_key(stored_key)
                        &&& k.cmp_spec(&stored_key) is Equal
                        &&& old_value == old_m@[stored_key]
                        &&& final_m@ == old_m@.insert(stored_key, v)

                    }
                }
                None => (
                    &&& forall |stored_key: Key| (
                        #[trigger] old_m@.contains_key(stored_key)
                            ==> !(k.cmp_spec(&stored_key) is Equal)
                    )
                    &&& final_m@ == old_m@.insert(k, v)

                ),
            }

        }
}