∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {γ : Sort w} (f : Std.DHashMap α β → γ)
  (h : ∀ (a b : Std.DHashMap α β), a.Equiv b → f a = f b) (m : Std.ExtDHashMap α β),
  Std.ExtDHashMap.lift f h m = Quotient.lift f h m.inner