Equation Of Motion unique

lemma equationOfMotion_unique (x y : Time → EuclideanSpace ℝ (Fin 1))    (hx : ContDiff ℝ ∞ x) (hy : ContDiff ℝ ∞ y)    (hEOMx : S.EquationOfMotion x) (hEOMy : S.EquationOfMotion y)    (h0 : x 0 = y 0) (hv0 : ∂ₜ x 0 = ∂ₜ y 0) :    x = y := by  have hIC : (fun τ : ℝ => (x (Time.toRealCLE.symm τ), ∂ₜ x (Time.toRealCLE.symm τ))) 0 =      (fun τ : ℝ => (y (Time.toRealCLE.symm τ), ∂ₜ y (Time.toRealCLE.symm τ))) 0 := by    have h00 : Time.toRealCLE.symm (0 : ℝ) = (0 : Time) := map_zero Time.toRealCLE.symm    simp only [h00, h0, hv0]  have hEq := ODE_solution_unique_univ    (v := fun _ p => S.phaseVectorField p) (s := fun _ => Set.univ) (t₀ := (0 : ℝ))    (f := fun τ : ℝ => (x (Time.toRealCLE.symm τ), ∂ₜ x (Time.toRealCLE.symm τ)))    (g := fun τ : ℝ => (y (Time.toRealCLE.symm τ), ∂ₜ y (Time.toRealCLE.symm τ)))    (fun _ => S.phaseVectorField.lipschitz.lipschitzOnWith)    (fun τ => ⟨S.phaseCurve_hasDerivAt x hx hEOMx τ, Set.mem_univ _⟩)    (fun τ => ⟨S.phaseCurve_hasDerivAt y hy hEOMy τ, Set.mem_univ _⟩)    hIC  funext t  have h1 := congrFun hEq (Time.toRealCLE t)  simp only [ContinuousLinearEquiv.symm_apply_apply] at h1  exact (Prod.ext_iff.mp h1).1