在 stdpp 库中找不到集合相等的引理

Question

我正在使用 stdpp 库，我想展示这两个集合的相等性：

{[x0]} ∪ dom X = {[x0]} ∪ dom Y

但是，我无法在 stdpp 中找到引理来将问题简化为：

dom X = dom Y

然后我就可以解决这个问题。 有人可以引导我找到丢失的引理吗？

Answer 1

解决方案是使用策略 f_equal，由评论提供 皮埃尔·卡斯泰兰。