Definition integerU32Vec3TWF (t : integerU32Vec3T) : Prop :=
     isU32 (u32vec3_0 t) 
  /\ isU32 (u32vec3_1 t)
  /\ isU32 (u32vec3_2 t).
