{α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.LawfulEqOrd α] →
        (k : α) →
          (Option (β k) → Option (β k)) →
            (t : Std.DTreeMap.Internal.Impl α β) →
              t.Balanced → Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (t.size - 1) (t.size + 1)