∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α → Ordering) (l : Std.DTreeMap.Internal.Impl α β) (k' : α)
  (v' : β k') (h : k k' = Ordering.eq),
  Std.DTreeMap.Internal.Impl.contains' k l = true → (Std.DTreeMap.Internal.Cell.ofEq k' v' ⋯).contains = true