Function btree_set_insert_ensures 

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

{
    obeys_cmp::<Key>() && btree_set_inv(old_m)
        ==> {
            &&& btree_set_inv(final_m)
            &&& if result {
                &&& forall |stored_key: Key| (
                    #[trigger] old_m@.contains(stored_key)
                        ==> !(k.cmp_spec(&stored_key) is Equal)
                )
                &&& final_m@ == old_m@.insert(k)

            } else {
                &&& exists |stored_key: Key| (
                    #[trigger] old_m@.contains(stored_key)
                        && k.cmp_spec(&stored_key) is Equal
                )
                &&& final_m@ == old_m@

            }

        }
}