∀ {α : 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_1 :
    {a : Std.DTreeMap.Internal.Impl α β} →
      {a_1 : Std.DTreeMap.Internal.Impl α β'} →
        (t : a.SameKeys a_1) → Std.DTreeMap.Internal.Impl.SameKeys.below t → Prop}
  {a : Std.DTreeMap.Internal.Impl α β} {a_1 : Std.DTreeMap.Internal.Impl α β'} {t : a.SameKeys a_1}
  (t_1 : Std.DTreeMap.Internal.Impl.SameKeys.below t),
  motive_1 ⋯ ⋯ →
    (∀ (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_2 : l.SameKeys l')
        (ih : Std.DTreeMap.Internal.Impl.SameKeys.below a) (a_ih : motive r r' a)
        (ih_1 : Std.DTreeMap.Internal.Impl.SameKeys.below a_2) (a_ih_1 : motive l l' a_2), motive_1 ⋯ ⋯) →
      motive_1 t t_1