∀ (_x : (n : ℕ) ×' BitVec n),
  BitVec.hash._unary _x =
    PSigma.casesOn _x fun n bv =>
      if n ≤ 64 then (↑bv.toFin).toUInt64
      else mixHash (↑bv.toFin).toUInt64 (BitVec.hash._unary ⟨n - 64, BitVec.setWidth (n - 64) (bv >>> 64)⟩)