Definition float16Vec4TWF (t : float16Vec4T) : Prop :=
     isValidFloat (f16vec4_0 t)
  /\ isValidFloat (f16vec4_1 t)
  /\ isValidFloat (f16vec4_2 t)
  /\ isValidFloat (f16vec4_3 t).
