Stream: new members
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
Last updated: May 08 2021 at 04:14 UTC