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: Oct 13 2024 at 01:02 UTC