{α : Type u_1} →
  {β : α → Type u_2} →
    (l : Std.DTreeMap.Internal.Impl α β) →
      (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.size > Std.DTreeMap.Internal.delta * l.size → Sort u_3) →
        (r : Std.DTreeMap.Internal.Impl α β) →
          (h : r.size > Std.DTreeMap.Internal.delta * l.size) →
            ((h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size) →
                motive Std.DTreeMap.Internal.Impl.leaf h) →
              ((size : ℕ) →
                  (rk : α) →
                    (rv : β rk) →
                      (rl rr : Std.DTreeMap.Internal.Impl α β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size >
                              Std.DTreeMap.Internal.delta * l.size) →
                          motive (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr) h) →
                motive r h