Definition integerS8Vec2TWF (t : integerS8Vec2T) : Prop :=
  isS8 (s8vec2_0 t) /\ isS8 (s8vec2_1 t).
