Definition integerU64Vec2TWF (t : integerU64Vec2T) : Prop :=
     isU64 (u64vec2_0 t) 
  /\ isU64 (u64vec2_1 t).
