{α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        {m : Array (Std.DHashMap.Internal.AssocList α β)} →
          {motive : Std.DHashMap.Internal.IsHashSelf m → Sort u_1} →
            (t : Std.DHashMap.Internal.IsHashSelf m) →
              ((hashes_to : ∀ (i : ℕ) (h : i < m.size), Std.DHashMap.Internal.List.HashesTo m[i].toList i m.size) →
                  motive ⋯) →
                motive t