{α : Type u_1} →
  {β : α → Type u_2} →
    (r' : Std.DTreeMap.Internal.Impl α β) →
      (szr : ℕ) →
        (k'' : α) →
          (v'' : β k'') →
            (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
              (motive :
                  Std.DTreeMap.Internal.Impl.Tree α β
                      (r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
                    Sort u_3) →
                (x :
                    Std.DTreeMap.Internal.Impl.Tree α β
                      (r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size)) →
                  ((ℓ : Std.DTreeMap.Internal.Impl α β) →
                      (hℓ₁ : ℓ.Balanced) →
                        (hℓ₂ : ℓ.size = r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
                          motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }) →
                    motive x