如何证明两个bv64位向量的逐位等价与整体等价等价？

我需要证明两个bv64位向量等价当且仅当它们的所有对应位都等价，即验证命题：
(a == b) == (forall i | 0 <= i < WORD_SIZE :: (BitIsSet(a, i) == BitIsSet(b, i)))

在Dafny中，a == b推导出所有对应位等价的正向情况很容易证明，但反向的难点在于：若a != b，需要证明存在i（满足0 <= i < 64）使得BitIsSet(a,i) != BitIsSet(b,i)。

BitIsSet的定义如下：

predicate method {:opaque} BitIsSet(x:bv64, i: nat)
    requires i < WORD_SIZE
{
   (x & ((1 as bv64) << (i as bv7))) != 0
}

我注意到布尔序列的等价性证明要简单得多，怀疑这是因为布尔序列用到了特定公理。同时我有个疑问：位向量的这个等价性命题无法证明，到底是因为Dafny缺少对应的公理，还是Boogie/Z3在位向量等价性验证上存在限制？

内容的提问来源于stack exchange，提问作者Reto Achermann