Definition integerU32Vec2TWF (t : integerU32Vec2T) : Prop :=
     isU32 (u32vec2_0 t) 
  /\ isU32 (u32vec2_1 t).
