Definition integerS8Vec3TWF (t : integerS8Vec3T) : Prop :=
     isS8 (s8vec3_0 t) 
  /\ isS8 (s8vec3_1 t)
  /\ isS8 (s8vec3_2 t).
