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