## Stream: math-comp users

### Topic: ✔ how ot use =i? in example undup s i= s

#### Andrey Klaus (Nov 12 2021 at 13:31):

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 ?

#### Andrey Klaus (Nov 12 2021 at 13:35):

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.

#### Laurent Théry (Nov 12 2021 at 13:37):

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.

#### Andrey Klaus (Nov 12 2021 at 14:38):

Great thank you! It is what I need.

#### Notification Bot (Nov 13 2021 at 23:18):

Andrey Klaus has marked this topic as resolved.

Last updated: Jan 29 2023 at 19:02 UTC