∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α},
  Std.Internal.List.containsKey k l = false →
    toInsert.contains k = false →
      Std.Internal.List.getKeyD k (Std.Internal.List.insertListIfNewUnit l toInsert) fallback = fallback