Search code examples
coq

Can't find Lemma for set equality in stdpp library

I am using the stdpp library and I want to show the equality of these two sets:

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

However, I cannot find a lemma in stdpp to reduce the problem to:

dom X = dom Y

which I then could solve. Could someone guide me to the missing Lemma?

Solution

  • The solution was to use the tactic f_equal, provided by the comment by Pierre Castéran.