## Stream: general

### Topic: Empty or not empty

#### Patrick Massot (Dec 17 2018 at 10:31):

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 (Dec 17 2018 at 10:38):

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 (Dec 17 2018 at 10:41):

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

Last updated: May 10 2021 at 19:16 UTC