HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector