∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α]
  (self : Array (Std.DHashMap.Internal.AssocList α β)) (i : USize) (hi : i.toNat < self.size),
  ∃ l,
    (List.flatMap Std.DHashMap.Internal.AssocList.toList self.toList).Perm (self[i.toNat].toList ++ l) ∧
      ∀ [LawfulHashable α],
        Std.DHashMap.Internal.IsHashSelf self →
          ∀ (k : α),
            (↑(Std.DHashMap.Internal.mkIdx self.size ⋯ (hash k))).toNat = i.toNat →
              Std.Internal.List.containsKey k l = false