∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, l.contains k = false → (Std.ExtDTreeMap.Const.unitOfList l cmp).getKey? k = none