Lemma integerU64Vec4TWFDecidable : forall (t : integerU64Vec4T), {integerU64Vec4TWF t}+{~integerU64Vec4TWF t}.
