Lemma float64Vec4TWFDecidable (t : float64Vec4T) : {float64Vec4TWF t}+{~float64Vec4TWF t}.
