寻求stdpp库中集合等式化简引理：将{[x0]}∪dom X={[x0]}∪dom Y转化为dom X=dom Y

• 核心解决路径：通过集合外延性分情况推导，或直接调用stdpp内置引理完成化简
• 可用引理及实操方法：
  1. 集合外延性引理ext：
     直接展开集合等式定义：∀ s t, s = t ↔ ∀ x, x ∈ s ↔ x ∈ t。将目标等式两边代入后分两种情况讨论：
     • 当x = x0时，两边均满足x ∈ {[x0]} ∪ dom X和x ∈ {[x0]} ∪ dom Y，条件自动成立；
     • 当x ≠ x0时，条件等价于x ∈ dom X ↔ x ∈ dom Y，直接推导出dom X = dom Y。
  2. union_eq_union_left引理：
     引理形式为：

     ∀ A B C, A ∪ B = A ∪ C ↔ B ⊆ A ∪ C ∧ C ⊆ A ∪ B
     

     代入A = {[x0]}、B = dom X、C = dom Y后，若已知x0 ∉ dom X且x0 ∉ dom Y，可搭配disjoint_singleton_left引理（x ∉ s → disjoint {x} s），将条件直接简化为dom X = dom Y。
  3. 基础引理组合推导：
     用singleton_union_eq（单元素集并集等价形式）配合subset_antisym（子集反对称性），先分别证明dom X ⊆ dom Y和dom Y ⊆ dom X，进而得到dom X = dom Y。

内容的提问来源于stack exchange，提问作者7Orion7