Lemma float16Vec3TWFDecidable (t : float16Vec3T) : {float16Vec3TWF t}+{~float16Vec3TWF t}.
