∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : BEq β]
  (m₁ m₂ : Std.DHashMap.Raw α fun x => β),
  Std.DHashMap.Raw.Const.beq m₁ m₂ =
    if h : 0 < m₁.buckets.size ∧ 0 < m₂.buckets.size then Std.DHashMap.Internal.Raw₀.Const.beq ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩
    else false