Lemma integerS8Vec2TWFDecidable : forall (t : integerS8Vec2T), {integerS8Vec2TWF t}+{~integerS8Vec2TWF t}.
