{α : Type u_1} →
  {β : α → Type u_2} →
    (r : Std.DTreeMap.Internal.Impl α β) →
      (motive :
          (l : Std.DTreeMap.Internal.Impl α β) →
            l.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Sort u_3) →
        (l : Std.DTreeMap.Internal.Impl α β) →
          (hl : l.Balanced) →
            (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size) →
              ((hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size) →
                    motive Std.DTreeMap.Internal.Impl.leaf hl hlr) →
                ((size : ℕ) →
                    (k' : α) →
                      (v' : β k') →
                        (l' r' : Std.DTreeMap.Internal.Impl α β) →
                          (hl : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) →
                            (hlr :
                                Std.DTreeMap.Internal.Impl.BalancedAtRoot
                                  (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size r.size) →
                              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hl hlr) →
                  motive l hl hlr