∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (n k : ℕ∞) (f : TestFunction Ω F n),
  k + 1 ≤ n → ContDiff ℝ (↑k) (fderiv ℝ ⇑f)