Definition integerS64Vec2TWF (t : integerS64Vec2T) : Prop :=
     isS64 (s64vec2_0 t) 
  /\ isS64 (s64vec2_1 t).
