Definition float64TWF (t : float64T) : Prop :=
  isValidFloat (f64 t).
