∀ {E : Type u_2} [inst : NormedAddCommGroup E] {F : Type u_3} [inst_1 : NormedAddCommGroup F] {s : Set E} {f : E → F}
  {x : E} {𝕜' : Type u_1} [inst_2 : NontriviallyNormedField 𝕜'] [inst_3 : NormedSpace 𝕜' E] [inst_4 : NormedSpace 𝕜' F]
  (motive : (n : WithTop ℕ∞) → ContDiffWithinAt 𝕜' n f s x → Prop) (n : WithTop ℕ∞) (h : ContDiffWithinAt 𝕜' n f s x),
  (∀ (h : ContDiffWithinAt 𝕜' ⊤ f s x), motive none h) →
    (∀ (n : ℕ∞) (h : ContDiffWithinAt 𝕜' (↑n) f s x), motive (some n) h) → motive n h