Definition float64Vec2TWF (t : float64Vec2T) : Prop :=
     isValidFloat (f64vec2_0 t)
  /\ isValidFloat (f64vec2_1 t).
