Axiom float16BitsOf : forall (r : R), Z.
