Definition integerU16Vec3TWF (t : integerU16Vec3T) : Prop :=
     isU16 (u16vec3_0 t) 
  /\ isU16 (u16vec3_1 t)
  /\ isU16 (u16vec3_2 t).
