∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α β)
  (x_1 : Std.DHashMap.Internal.AssocList.contains a x = true),
  Std.DHashMap.Internal.AssocList.getEntry a x x_1 =
    match x, x_1 with
    | Std.DHashMap.Internal.AssocList.cons k v es, h =>
      if hka : (k == a) = true then ⟨k, v⟩ else Std.DHashMap.Internal.AssocList.getEntry a es ⋯