Lemma integerU32Vec4TWFDecidable : forall (t : integerU32Vec4T), {integerU32Vec4TWF t}+{~integerU32Vec4TWF t}.
