Lemma integerS8Vec3TWFDecidable : forall (t : integerS8Vec3T), {integerS8Vec3TWF t}+{~integerS8Vec3TWF t}.
