-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.link!.induct_unfolding : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k)
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Prop),
  (∀ (r : Std.DTreeMap.Internal.Impl α β),
      motive Std.DTreeMap.Internal.Impl.leaf r (Std.DTreeMap.Internal.Impl.insertMin! k v r)) →
    (∀ (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') Std.DTreeMap.Internal.Impl.leaf
          (Std.DTreeMap.Internal.Impl.insertMax! k v (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r''))) →
      (∀ (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β) (sz'_1 : ℕ) (k'_1 : α)
          (v'_1 : β k'_1) (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β),
          Std.DTreeMap.Internal.delta * sz' < sz'_1 →
            motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') l''_1
                (Std.DTreeMap.Internal.Impl.link! k v (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') l''_1) →
              motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')
                (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)
                (Std.DTreeMap.Internal.Impl.balanceL! k'_1 v'_1
                  (Std.DTreeMap.Internal.Impl.link! k v (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') l''_1)
                  r''_1)) →
        (∀ (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β) (sz'_1 : ℕ) (k'_1 : α)
            (v'_1 : β k'_1) (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β),
            ¬Std.DTreeMap.Internal.delta * sz' < sz'_1 →
              Std.DTreeMap.Internal.delta * sz'_1 < sz' →
                motive r'' (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)
                    (Std.DTreeMap.Internal.Impl.link! k v r''
                      (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)) →
                  motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')
                    (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)
                    (Std.DTreeMap.Internal.Impl.balanceR! k' v' l''
                      (Std.DTreeMap.Internal.Impl.link! k v r''
                        (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)))) →
          (∀ (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β) (sz'_1 : ℕ) (k'_1 : α)
              (v'_1 : β k'_1) (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β),
              ¬Std.DTreeMap.Internal.delta * sz' < sz'_1 →
                ¬Std.DTreeMap.Internal.delta * sz'_1 < sz' →
                  motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')
                    (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)
                    (Std.DTreeMap.Internal.Impl.inner
                      ((Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').size + 1 +
                        (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1).size)
                      k v (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')
                      (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1))) →
            ∀ (l r : Std.DTreeMap.Internal.Impl α β), motive l r (Std.DTreeMap.Internal.Impl.link! k v l r)