Definition float32Vec2TWF (t : float32Vec2T) : Prop :=
     isValidFloat (f32vec2_0 t)
  /\ isValidFloat (f32vec2_1 t).
