∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {β : α → Type v} {a : Std.DTreeMap.Internal.Impl α β} (t : a.WF),
  (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} (a : t.Balanced) (a_1 : ∀ [Std.TransOrd α], t.Ordered),
      motive t ⋯) →
    (∀ {x : α → Type v}, motive Std.DTreeMap.Internal.Impl.empty ⋯) →
      (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k} (a : t.WF),
          motive (Std.DTreeMap.Internal.Impl.insert k v t h).impl ⋯) →
        (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k} (a : t.WF),
            motive (Std.DTreeMap.Internal.Impl.insertIfNew k v t h).impl ⋯) →
          (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} (a : t.WF),
              motive (Std.DTreeMap.Internal.Impl.erase k t h).impl ⋯) →
            (∀ {x : α → Type v} [inst_1 : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced}
                {k : α} {f : Option (x k) → Option (x k)} (a : t.WF),
                motive (Std.DTreeMap.Internal.Impl.alter k f t h).impl ⋯) →
              (∀ {x : Type v} {t : Std.DTreeMap.Internal.Impl α fun x_1 => x} {h : t.Balanced} {k : α}
                  {f : Option x → Option x} (a : t.WF),
                  motive (Std.DTreeMap.Internal.Impl.Const.alter k f t h).impl ⋯) →
                (∀ {x : α → Type v} [inst_1 : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α x} {k : α}
                    {f : x k → x k} (a : t.WF), motive (Std.DTreeMap.Internal.Impl.modify k f t) ⋯) →
                  (∀ {x : Type v} {t : Std.DTreeMap.Internal.Impl α fun x_1 => x} {k : α} {f : x → x} (a : t.WF),
                      motive (Std.DTreeMap.Internal.Impl.Const.modify k f t) ⋯) →
                    (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k}
                        (a : t.WF), motive (Std.DTreeMap.Internal.Impl.containsThenInsert k v t h).2.impl ⋯) →
                      (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k}
                          (a : t.WF), motive (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v t h).2.impl ⋯) →
                        (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced}
                            {f : (a : α) → x a → Bool} (a : t.WF),
                            motive (Std.DTreeMap.Internal.Impl.filter f t h).impl ⋯) →
                          (∀ {x : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α x} {f : (a : α) → x a → x a → x a}
                              {h : t₁.Balanced} [inst_1 : Std.LawfulEqOrd α] (a : t₁.WF),
                              motive (Std.DTreeMap.Internal.Impl.mergeWith f t₁ t₂ h).impl ⋯) →
                            (∀ {x : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x_1 => x} {f : α → x → x → x}
                                {h : t₁.Balanced} (a : t₁.WF),
                                motive (Std.DTreeMap.Internal.Impl.Const.mergeWith f t₁ t₂ h).impl ⋯) →
                              (∀ {x : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α x} {h : t₁.Balanced}
                                  (a : t₁.WF), motive (t₁.inter t₂ h) ⋯) →
                                motive a t