∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a a_1 : α) (b : β a_1) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getKey? a (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if (a_1 == a) = true then some a_1 else Std.DHashMap.Internal.AssocList.getKey? a es