Definition integerU8Vec2TWF (t : integerU8Vec2T) : Prop :=
     isU8 (u8vec2_0 t) 
  /\ isU8 (u8vec2_1 t).
