0

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?

2
  • 2
    Did you try to call the tactic f_equal? Oct 27 at 7:05
  • Thanks! That actually solved my problem.
    – 7Orion7
    Oct 27 at 9:26

1 Answer 1

0

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

1
  • Your answer could be improved with additional supporting information. Please edit to add further details, such as citations or documentation, so that others can confirm that your answer is correct. You can find more information on how to write good answers in the help center.
    – Community Bot
    Oct 30 at 16:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.