Lemma integerU8Vec4TWFDecidable : forall (t : integerU8Vec4T), {integerU8Vec4TWF t}+{~integerU8Vec4TWF t}.
