Expand Equiv subtypes to include sum types up to arity 22

[jdegoes]

A sum type requires a fallible deconstructor and infallible constructor for each term. Or more if we want totality checking at compile-time.

[jdegoes]

The corresponding idea and prototype for product types is located here and can inform this issue.

[ghost]

I can prolly do this one.