∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (b : β a) (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.replace a b x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => Std.DHashMap.Internal.AssocList.nil
    | Std.DHashMap.Internal.AssocList.cons k v l =>
      bif k == a then Std.DHashMap.Internal.AssocList.cons a b l
      else Std.DHashMap.Internal.AssocList.cons k v (Std.DHashMap.Internal.AssocList.replace a b l)