∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (ho : t.Ordered) (he : ∃ a ∈ t, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.getEntryGT k t ho he = Std.DTreeMap.Internal.Impl.getEntryGT k_1 t_1 ⋯ ⋯