{α : Type u_1} →
  {β : α → Type u_2} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        (a : α) →
          (motive : (m : Std.DHashMap.Internal.Raw₀ α β) → m.contains a = true → Sort u_3) →
            (m : Std.DHashMap.Internal.Raw₀ α β) →
              (hma : m.contains a = true) →
                ((size : ℕ) →
                    (buckets : Array (Std.DHashMap.Internal.AssocList α β)) →
                      (h : 0 < { size := size, buckets := buckets }.buckets.size) →
                        (hma : Std.DHashMap.Internal.Raw₀.contains ⟨{ size := size, buckets := buckets }, h⟩ a = true) →
                          motive ⟨{ size := size, buckets := buckets }, h⟩ hma) →
                  motive m hma