∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {motive_1 :
    {β : α → Type v} → {a : Std.DTreeMap.Internal.Impl α β} → (t : a.WF) → Std.DTreeMap.Internal.Impl.WF.below t → Prop}
  {β : α → Type v} {a : Std.DTreeMap.Internal.Impl α β} {t : a.WF} (t_1 : Std.DTreeMap.Internal.Impl.WF.below t),
  (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} (a : t.Balanced) (a_1 : ∀ [Std.TransOrd α], t.Ordered),
      motive_1 ⋯ ⋯) →
    (∀ {x : α → Type v}, motive_1 ⋯ ⋯) →
      (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k} (a : t.WF)
          (ih : Std.DTreeMap.Internal.Impl.WF.below a) (a_ih : motive t a), motive_1 ⋯ ⋯) →
        (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k} (a : t.WF)
            (ih : Std.DTreeMap.Internal.Impl.WF.below a) (a_ih : motive t a), motive_1 ⋯ ⋯) →
          (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} (a : t.WF)
              (ih : Std.DTreeMap.Internal.Impl.WF.below a) (a_ih : motive t a), motive_1 ⋯ ⋯) →
            (∀ {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) (ih : Std.DTreeMap.Internal.Impl.WF.below a)
                (a_ih : motive t a), motive_1 ⋯ ⋯) →
              (∀ {x : Type v} {t : Std.DTreeMap.Internal.Impl α fun x_1 => x} {h : t.Balanced} {k : α}
                  {f : Option x → Option x} (a : t.WF) (ih : Std.DTreeMap.Internal.Impl.WF.below a) (a_ih : motive t a),
                  motive_1 ⋯ ⋯) →
                (∀ {x : α → Type v} [inst_1 : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α x} {k : α}
                    {f : x k → x k} (a : t.WF) (ih : Std.DTreeMap.Internal.Impl.WF.below a) (a_ih : motive t a),
                    motive_1 ⋯ ⋯) →
                  (∀ {x : Type v} {t : Std.DTreeMap.Internal.Impl α fun x_1 => x} {k : α} {f : x → x} (a : t.WF)
                      (ih : Std.DTreeMap.Internal.Impl.WF.below a) (a_ih : motive t a), motive_1 ⋯ ⋯) →
                    (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k}
                        (a : t.WF) (ih : Std.DTreeMap.Internal.Impl.WF.below a) (a_ih : motive t a), motive_1 ⋯ ⋯) →
                      (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k}
                          (a : t.WF) (ih : Std.DTreeMap.Internal.Impl.WF.below a) (a_ih : motive t a), motive_1 ⋯ ⋯) →
                        (∀ {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced}
                            {f : (a : α) → x a → Bool} (a : t.WF) (ih : Std.DTreeMap.Internal.Impl.WF.below a)
                            (a_ih : motive t a), motive_1 ⋯ ⋯) →
                          (∀ {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)
                              (ih : Std.DTreeMap.Internal.Impl.WF.below a) (a_ih : motive t₁ a), motive_1 ⋯ ⋯) →
                            (∀ {x : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x_1 => x} {f : α → x → x → x}
                                {h : t₁.Balanced} (a : t₁.WF) (ih : Std.DTreeMap.Internal.Impl.WF.below a)
                                (a_ih : motive t₁ a), motive_1 ⋯ ⋯) →
                              (∀ {x : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α x} {h : t₁.Balanced} (a : t₁.WF)
                                  (ih : Std.DTreeMap.Internal.Impl.WF.below a) (a_ih : motive t₁ a), motive_1 ⋯ ⋯) →
                                motive_1 t t_1