∀ {α : Type u} {β : α → Type v}
  (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → (n : ℕ) → n < t.size → (a : α) × β a → Prop),
  (∀ (size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
      (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
      (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) (h_1 : compare n l'.size = Ordering.lt),
      motive l' ⋯ n ⋯ (l'.entryAtIdx ⋯ n ⋯) →
        motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h (l'.entryAtIdx ⋯ n ⋯)) →
    (∀ (size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
        (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
        (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size),
        compare n l'.size = Ordering.eq → motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h ⟨k, v⟩) →
      (∀ (size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
          (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
          (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) (h_1 : compare n l'.size = Ordering.gt),
          motive r' ⋯ (n - l'.size - 1) ⋯ (r'.entryAtIdx ⋯ (n - l'.size - 1) ⋯) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h (r'.entryAtIdx ⋯ (n - l'.size - 1) ⋯)) →
        ∀ (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced) (n : ℕ) (h : n < t.size),
          motive t hl n h (t.entryAtIdx hl n h)