Lemma integerS64Vec3TWFDecidable : forall (t : integerS64Vec3T), {integerS64Vec3TWF t}+{~integerS64Vec3TWF t}.
