Lemma integerS16Vec4TWFDecidable : forall (t : integerS16Vec4T), {integerS16Vec4TWF t}+{~integerS16Vec4TWF t}.
