{α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.LawfulEqOrd α] →
        ((a : α) → β a → β a → β a) →
          (t₁ : Std.DTreeMap.Internal.Impl α β) →
            Std.DTreeMap.Internal.Impl α β → t₁.Balanced → Std.DTreeMap.Internal.Impl.BalancedTree α β