Lemma integerS64Vec2TWFDecidable : forall (t : integerS64Vec2T), {integerS64Vec2TWF t}+{~integerS64Vec2TWF t}.
