Lemma integerS8Vec4TWFDecidable : forall (t : integerS8Vec4T), {integerS8Vec4TWF t}+{~integerS8Vec4TWF t}.
