Lemma float16TWFDecidable (t : float16T) : {float16TWF t}+{~float16TWF t}.
