∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.isEmpty = false),
  Std.DTreeMap.Internal.Impl.Const.minEntry x x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => (k, v)
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      h_1 => Std.DTreeMap.Internal.Impl.Const.minEntry l ⋯