Definition integerS32Vec2TWF (t : integerS32Vec2T) : Prop :=
     isS32 (s32vec2_0 t) 
  /\ isS32 (s32vec2_1 t).
