Pattern matching on enums with a list of alternatives

[skeuchel]

For pattern matching on unions, we have a version that allows to provide a list of alternatives.

https://github.com/katamaran-project/katamaran/blob/f97ef7e664dc74c89dc3f1e19652c1d5b0f7b81a/theories/Syntax/Statements.v#L181-L182

This list is checked to be exhaustive by a type-level computation

https://github.com/katamaran-project/katamaran/blob/f97ef7e664dc74c89dc3f1e19652c1d5b0f7b81a/theories/Syntax/Statements.v#L163-L167

We currently do not have the same functionality for enums which should be added.

This is useful for replacing the fixed size notations that we use, which sometimes need extension when an enum is extended, e.g. in https://github.com/katamaran-project/katamaran/pull/43, which is annoying.