Special syntax for nested/sequence of sum_CASE constants

[mn200]

So that

case x of
  | INL se => sexp_size se
  | INR (INL se) => sexp_size se
  | INR (INR (INL ses)) => list_size sexp_size ses
  | INR (INR (INR (INL ses))) => list_size sexp_size ses
  | INR (INR (INR (INR (INL ses)))) => list_size sexp_size ses
  | INR (INR (INR (INR (INR (INL ses))))) => list_size sexp_size ses
  | INR (INR (INR (INR (INR (INR (INL se_opt))))) => option_size se_opt
  | INR (INR (INR (INR (INR (INR (INR (INL se))))))) => sexp_size se
  | INR (INR (INR (INR (INR (INR (INR (INR ses))))))) => list_size sexp_size ses

could be written as

nested_sum_case x of
  | se => sexp_size se
  | se => sexp_size se
  | ses => list_size sexp_size ses
  | ses => list_size sexp_size ses
  | ses => list_size sexp_size ses
  | ses => list_size sexp_size ses
  | se_opt => option_size se_opt
  | se => sexp_size se
  | ses => list_size sexp_size ses

or similar. With the name nested_sum_case obviously up for bike-shedding. Thanks to @myreen and discussion at recent HOL workshop for idea.