-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.link2.fun_cases : ∀ {α : Type u} {β : α → Type v} (motive : (l r : Std.DTreeMap.Internal.Impl α β) → l.Balanced → r.Balanced → Prop),
  (∀ (r : Std.DTreeMap.Internal.Impl α β) (hr : r.Balanced) (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
      Std.DTreeMap.Internal.Impl.leaf.Balanced → motive Std.DTreeMap.Internal.Impl.leaf r hr_1 hr) →
    (∀ (szr : ℕ) (k'' : α) (v'' : β k'') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
        (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced)
        (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
        (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced →
          Std.DTreeMap.Internal.Impl.leaf.Balanced →
            motive (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') Std.DTreeMap.Internal.Impl.leaf hr hr_1) →
      (∀ (szr : ℕ) (k'' : α) (v'' : β k'') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
          (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced) (szr_1 : ℕ) (k''_1 : α)
          (v''_1 : β k''_1) (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β)
          (hr_1 : (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).Balanced),
          Std.DTreeMap.Internal.delta * szr < szr_1 →
            ∀ (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced),
              (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced →
                ∀ (hℓ₂ : ℓ.size = (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size + l''_1.size),
                  (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).Balanced →
                    (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').link2 l''_1 ⋯ ⋯ =
                        { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } →
                      motive (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'')
                        (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1) hr hr_1) →
        (∀ (szr : ℕ) (k'' : α) (v'' : β k'') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
            (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced) (szr_1 : ℕ) (k''_1 : α)
            (v''_1 : β k''_1) (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β)
            (hr_1 : (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).Balanced),
            ¬Std.DTreeMap.Internal.delta * szr < szr_1 →
              Std.DTreeMap.Internal.delta * szr_1 < szr →
                ∀ (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced),
                  (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced →
                    (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).Balanced →
                      ∀
                        (hℓ₂ :
                          ℓ.size = r''.size + (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).size),
                        r''.link2 (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1) ⋯ ⋯ =
                            { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } →
                          motive (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'')
                            (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1) hr hr_1) →
          (∀ (szr : ℕ) (k'' : α) (v'' : β k'') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
              (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced) (szr_1 : ℕ) (k''_1 : α)
              (v''_1 : β k''_1) (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β)
              (hr_1 : (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).Balanced),
              ¬Std.DTreeMap.Internal.delta * szr < szr_1 →
                ¬Std.DTreeMap.Internal.delta * szr_1 < szr →
                  (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced →
                    (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).Balanced →
                      motive (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'')
                        (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1) hr hr_1) →
            ∀ (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (hr : r.Balanced), motive l r hl hr