Definition integerU64Vec4TWF (t : integerU64Vec4T) : Prop :=
     isU64 (u64vec4_0 t) 
  /\ isU64 (u64vec4_1 t)
  /\ isU64 (u64vec4_2 t)
  /\ isU64 (u64vec4_3 t).
