Definition integerS16Vec2TWF (t : integerS16Vec2T) : Prop :=
     isS16 (s16vec2_0 t) 
  /\ isS16 (s16vec2_1 t).
