x \in undup s, I would like to prove
x \in s. What I found about it is that
undup s i= s. How to prove that
x \in s ?
I mean is there a way to use
undup s i= s for this proof or should I use the induction? If there is such way, it would be greate to have an example.
If you have
H : undup s =i s, you can use it to rewrite, try to see what
=i means by setting
have H1 := H x.
Great thank you! It is what I need.
Andrey Klaus has marked this topic as resolved.
Last updated: Jan 29 2023 at 19:02 UTC