Showing X is a subset of itself

Stream: new members

[Anna Hollands]

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]

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

[Patrick Massot]

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