Empty or not empty

Stream: general

[Patrick Massot]

How can I prove something by case splitting depending on whether or not a type is inhabited? I know about the inhabited and nonempty classes, but it looks like I can't do anything when I assume not (nonempty a) or not (inhabited a). So what I do is by_cases H : ∃ x : α, true,. Is that right?

[Chris Hughes]

You can prove a -> false from h : not (nonempty a), it's just assume x, h ⟨x⟩. Not sure what else you'd need apart from this.

[Patrick Massot]

Strange, I thought I tried that. Thanks! I does look slightly less stupid that way