∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} (a a_1 : List ((a : α) × β a)),
  a = a_1 →
    ∀ (a_2 : α) (a_3 : k a_2 = Ordering.gt) (a_4 a_5 : β a_2),
      a_4 = a_5 →
        Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_2 a_3 a_4 =
          Std.DTreeMap.Internal.Impl.ExplorationStep.gt a_1 a_2 a_3 a_5