{α : Type u_2} →
  {β : α → Type u_1} →
    [inst : BEq α] →
      (a : α) →
        (motive :
            (x : Std.DHashMap.Internal.AssocList α β) →
              Std.DHashMap.Internal.AssocList.contains a x = true → Sort u_3) →
          (x : Std.DHashMap.Internal.AssocList α β) →
            (x_1 : Std.DHashMap.Internal.AssocList.contains a x = true) →
              ((k : α) →
                  (v : β k) →
                    (es : Std.DHashMap.Internal.AssocList α β) →
                      (h :
                          Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) =
                            true) →
                        motive (Std.DHashMap.Internal.AssocList.cons k v es) h) →
                motive x x_1