∀ {α : Type u} {β : α → Type v} [inst : Hashable α]
  (motive : ℕ → Array (Std.DHashMap.Internal.AssocList α β) → { d // 0 < d.size } → Prop),
  (∀ (i : ℕ) (source : Array (Std.DHashMap.Internal.AssocList α β)) (target : { d // 0 < d.size })
      (h : i < source.size),
      have es := source[i];
      have source_1 := source.set i Std.DHashMap.Internal.AssocList.nil h;
      have target_1 := Std.DHashMap.Internal.AssocList.foldl (Std.DHashMap.Internal.Raw₀.reinsertAux hash) target es;
      motive (i + 1) source_1 target_1 → motive i source target) →
    (∀ (i : ℕ) (source : Array (Std.DHashMap.Internal.AssocList α β)) (target : { d // 0 < d.size }),
        ¬i < source.size → motive i source target) →
      ∀ (i : ℕ) (source : Array (Std.DHashMap.Internal.AssocList α β)) (target : { d // 0 < d.size }),
        motive i source target