Lemma float64Vec2TWFDecidable (t : float64Vec2T) : {float64Vec2TWF t}+{~float64Vec2TWF t}.
