{α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      [inst : Ord α] →
        (k : α) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            ((c : Std.DTreeMap.Internal.Cell α β (compare k)) →
                (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → δ) →
              δ