Lemma float64TWFDecidable (t : float64T) : {float64TWF t}+{~float64TWF t}.
