Question

How do I pattern match against a head and tail of a sequence or against a set?

Answer

You can’t. Match expressions and statements operate on datatype values and not on other Dafny types like sets, sequences, and maps. If statements, perhaps with binding guards, may be an alternative.