∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v' : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  compare k k' = Ordering.lt →
    ∀ (c : Std.DTreeMap.Internal.Cell α β (compare k)),
      (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) →
        Std.DTreeMap.Internal.Impl.contains' (compare k) (Std.DTreeMap.Internal.Impl.inner size k' v' l r) = true →
          c.contains = true