∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β)
  (r : t.IteratedSlowInsertionInto) (a : α) (b : β a) {P : Std.DTreeMap.Internal.Impl α β → Prop},
  P t →
    (∀ (t'' : Std.DTreeMap.Internal.Impl α β) (a : α) (b : β a),
        P t'' → P (Std.DTreeMap.Internal.Impl.insert! a b t'')) →
      P (Std.DTreeMap.Internal.Impl.insert! a b ↑r)