Function btree_set_inv 

pub open spec fn btree_set_inv<Key: Ord, A: Allocator + Clone>(
    m: &BTreeSet<Key, A>,
) -> bool

{
    forall |k1: Key, k2: Key| (
        {
            &&& #[trigger] m@.contains(k1)
            &&& #[trigger] m@.contains(k2)
            &&& k1 != k2

        } ==> !(k1.cmp_spec(&k2) is Equal)
    )
}