{α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {k : α → Ordering} →
        {motive : Std.DTreeMap.Internal.Impl.ExplorationStep α β k → Sort u_1} →
          (t : Std.DTreeMap.Internal.Impl.ExplorationStep α β k) →
            ((a : α) →
                (a_1 : k a = Ordering.lt) →
                  (a_2 : β a) →
                    (a_3 : List ((a : α) × β a)) →
                      motive (Std.DTreeMap.Internal.Impl.ExplorationStep.lt a a_1 a_2 a_3)) →
              ((a : List ((a : α) × β a)) →
                  (a_1 : Std.DTreeMap.Internal.Cell α β k) →
                    (a_2 : List ((a : α) × β a)) → motive (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_1 a_2)) →
                ((a : List ((a : α) × β a)) →
                    (a_1 : α) →
                      (a_2 : k a_1 = Ordering.gt) →
                        (a_3 : β a_1) → motive (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3)) →
                  motive t