Definition integerU64Vec3TWF (t : integerU64Vec3T) : Prop :=
     isU64 (u64vec3_0 t) 
  /\ isU64 (u64vec3_1 t)
  /\ isU64 (u64vec3_2 t).
