Error in `f1_equal_to_f2`. Should be ` f1_equal_to_f2 : forall (x: Float), floatToR(f1(x)) = f2(floatToR(x))` with an implicit proof delivered to `f2` that `forall (x: R), IsFloat(floatToR(x))`.

Also there's some subtleties in how to set up the code extraction to make sure you don't inadvertently extract other real-valued functions, but this is already too long.