Lemma float64Vec3TWFDecidable (t : float64Vec3T) : {float64Vec3TWF t}+{~float64Vec3TWF t}.
