{α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : α) →
          ((fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l : Std.DTreeMap.Internal.Impl α β) →
                      (x : α) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (l r : Std.DTreeMap.Internal.Impl α β) →
                        (size_1 : ℕ) →
                          (k_1 : α) →
                            (v_1 : β k_1) →
                              (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                                (h : r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) →
                                  (fallback : α) →
                                    motive
                                      (Std.DTreeMap.Internal.Impl.inner size k v l
                                        (namedPattern r (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) h))
                                      fallback) →
                motive x x_1