{α : Type u_1} →
  {β : α → Type u_2} →
    (sofar : { t // t.Balanced }) →
      (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (↑sofar).size ((↑sofar).size + 1) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (↑sofar).size ((↑sofar).size + 1)) →
          ((val : Std.DTreeMap.Internal.Impl α β) →
              (prop : val.Balanced) →
                (lb_le_size_impl : (↑sofar).size ≤ val.size) →
                  (size_impl_le_ub : val.size ≤ (↑sofar).size + 1) →
                    motive
                      { impl := val, balanced_impl := prop, lb_le_size_impl := lb_le_size_impl,
                        size_impl_le_ub := size_impl_le_ub }) →
            motive x