How to reason about equality between different datatypes?

Question

I am working on a verification project where the specification uses the following inductive datatype to represent bitvectors (MIT's bbv)

Inductive word : nat -> Set :=
| WO : word O
| WS : bool -> forall n, word n -> word (S n).

On the implementation side, however, the EDSL I am using uses Coq's stdlib Vector to represent bitvectors (with type parameter A set to bool)

Inductive t A : nat -> Type :=
  |nil : t A 0
  |cons : forall (h:A) (n:nat), t A n -> t A (S n).

In order to compare the behavior of functions on the implementation side with the spec correspondents, I need to be able to reason about equality between these different datatypes. I have therefore written the following recursive Prop, which will generate a rewritable bool equality for each bit in the bitvectors.

Fixpoint eq_bbvword_bvector {sz} : word sz -> Bvector sz -> Prop :=
        match sz with
        | 0 => fun _ _ => True
        | S n => fun w bv => (whd w) = (Vector.hd bv) /\
        eq_bbvword_bvector (@wtl n w) (Vector.tl bv)
        end.

This works fine, but I wanted to able to work with rewritable equalities between word and Bvector (alias for Vector bool) instead of always referring to this predicate to compare.

Any tips on how to do this ?