Multiple wildcard arms in `cases` not supported

[digama0]

this works:

example (h : P ∨ Q) : True := by
  cases h 
  case _ hpq => trivial
  case _ hpr => trivial

but this doesn't:

example (h : P ∨ Q) : True := by
  cases h with -- invalid occurrence of wildcard alternative, it must be the last alternative
  | _ hpq => trivial
  | _ hpr => trivial

I think that cases / induction should use a similar strategy to case here: non-terminal wildcard alternatives should apply to the first remaining constructor. Only the last wildcard alternative should run on all remaining constructors.

This makes it usable for pattern matching on an inductive without having to say what the name of the constructors are.