bvector_eqdec: found a better way

The two major cases in bvector_eqdec reduce to cases in which the heads
of bvectors are not equal, or the tails of bvectors are not equal.
Separate those into two different lemmas, and write bvector_eqdec in
terms of those.
Merge pull request #1 from frenetic-lang/bvector_eqdec

bvector_eqdec: found a better way