Definition float64Vec3TWF (t : float64Vec3T) : Prop :=
     isValidFloat (f64vec3_0 t)
  /\ isValidFloat (f64vec3_1 t)
  /\ isValidFloat (f64vec3_2 t).
