Lemma integerU64Vec2TWFDecidable : forall (t : integerU64Vec2T), {integerU64Vec2TWF t}+{~integerU64Vec2TWF t}.
