Lemma float16Vec4TWFDecidable (t : float16Vec4T) : {float16Vec4TWF t}+{~float16Vec4TWF t}.
