∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {a b δ : ℝ},
  (∀ t ∈ Set.Ico a b, LipschitzOnWith K (v t) (s t)) →
    ContinuousOn f (Set.Icc a b) →
      (∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) →
        (∀ t ∈ Set.Ico a b, f t ∈ s t) →
          ContinuousOn g (Set.Icc a b) →
            (∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) →
              (∀ t ∈ Set.Ico a b, g t ∈ s t) →
                dist (f a) (g a) ≤ δ → ∀ t ∈ Set.Icc a b, dist (f t) (g t) ≤ δ * Real.exp (↑K * (t - a))