∀ {n : WithTop ℕ∞} {E : Type u_11} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_12}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_13} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {f g : ℝ → M} {s : ℝ},
  ContMDiff (modelWithCornersSelf ℝ ℝ) I n f →
    ContMDiff (modelWithCornersSelf ℝ ℝ) I n g →
      f =ᶠ[nhds s] g → ContMDiff (modelWithCornersSelf ℝ ℝ) I n ((Set.Iic s).piecewise f g)