∀ {α : Type u} {β : Type v} [inst : BEq α] (a k : α) (v : β) (es : Std.DHashMap.Internal.AssocList α fun x => β)
  (h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) = true),
  Std.DHashMap.Internal.AssocList.get a (Std.DHashMap.Internal.AssocList.cons k v es) h =
    if hka : (k == a) = true then v else Std.DHashMap.Internal.AssocList.get a es ⋯