Lemma integerS32Vec4TWFDecidable : forall (t : integerS32Vec4T), {integerS32Vec4TWF t}+{~integerS32Vec4TWF t}.
