Hello.

I have `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