∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → ∀ {h' : k' ∈ Std.TreeMap.unitOfList l cmp}, (Std.TreeMap.unitOfList l cmp).getKey k' h' = k