∀ {α : Type u} {β : α → Type v} {γ : Type w} [inst : Ord α] (k : α → Ordering) (init : γ)
  (inner : γ → Std.DTreeMap.Internal.Impl.ExplorationStep α β k → γ) (l : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.explore k init inner l =
    match l with
    | Std.DTreeMap.Internal.Impl.leaf =>
      inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.eq [] Std.DTreeMap.Internal.Cell.empty [])
    | Std.DTreeMap.Internal.Impl.inner size ky y l r =>
      match h : k ky with
      | Ordering.lt =>
        Std.DTreeMap.Internal.Impl.explore k
          (inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.lt ky h y r.toListModel)) inner l
      | Ordering.eq =>
        inner init
          (Std.DTreeMap.Internal.Impl.ExplorationStep.eq l.toListModel (Std.DTreeMap.Internal.Cell.ofEq ky y ⋯)
            r.toListModel)
      | Ordering.gt =>
        Std.DTreeMap.Internal.Impl.explore k
          (inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.gt l.toListModel ky h y)) inner r