Definition integerU16Vec2TWF (t : integerU16Vec2T) : Prop :=
     isU16 (u16vec2_0 t) 
  /\ isU16 (u16vec2_1 t).
