∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1}
  {motive : (a : Std.DTreeMap.Internal.Impl α β) → (a_1 : Std.DTreeMap.Internal.Impl α β') → a.SameKeys a_1 → Prop},
  motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf ⋯ →
    (∀ (sz : ℕ) (k : α) (v : β k) (v' : β' k) (r : Std.DTreeMap.Internal.Impl α β)
        (r' : Std.DTreeMap.Internal.Impl α β') (l : Std.DTreeMap.Internal.Impl α β)
        (l' : Std.DTreeMap.Internal.Impl α β') (a : r.SameKeys r') (a_1 : l.SameKeys l'),
        motive r r' a →
          motive l l' a_1 →
            motive (Std.DTreeMap.Internal.Impl.inner sz k v l r) (Std.DTreeMap.Internal.Impl.inner sz k v' l' r') ⋯) →
      ∀ {a : Std.DTreeMap.Internal.Impl α β} {a_1 : Std.DTreeMap.Internal.Impl α β'} (t : a.SameKeys a_1),
        motive a a_1 t