## Stream: new members

### Topic: Showing X is a subset of itself

#### Anna Hollands (Jun 29 2020 at 23:10):

Hi! I'm trying to prove a lemma that requires me to find a subset of a set X st.... X works, but use X doesn't. How do I get it to recognise X as a valid subset of X?

#### Patrick Massot (Jun 29 2020 at 23:11):

(univ : set X) is what you are looking for.

#### Patrick Massot (Jun 29 2020 at 23:12):

X has type Type u for some universe u. It doesn't have type set X.

Last updated: May 08 2021 at 04:14 UTC