Rookie question

Stream: general

[Frank Mobler]

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.

[Mario Carneiro]

or.inl rfl is a proof term for that

[Mario Carneiro]

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

[Frank Mobler]

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