Zulip Chat Archive

Stream: general

Topic: Rookie question


view this post on Zulip Frank Mobler (May 22 2018 at 05:26):

I'm stumped proving example {V : Type}{n : V} : n ∈ ({n} : set V). Please without tactics first. I want to see how to construct proof terms explicitly for types like this.

view this post on Zulip Mario Carneiro (May 22 2018 at 05:34):

or.inl rfl is a proof term for that

view this post on Zulip Mario Carneiro (May 22 2018 at 05:35):

because the goal is defeq to n = n \/ false:

example {V : Type} {n : V} : n ∈ ({n} : set V) :=
show n = n ∨ false, from or.inl rfl

view this post on Zulip Frank Mobler (May 22 2018 at 05:37):

Aha. This helps a lot. Light bulbs going on. Thanks.


Last updated: May 14 2021 at 00:42 UTC