Experimental support for n-way sum types.

Added sum types to the mix. Again, performance is dismal, but I am kind of happy I figured the types out.

I also finally have Coq code for these combinators without any undefined holes. As you see, they are very general, work in terms of binary `pair`, `choice` and `wrap`. My hope is that the Coq definition will help to:

1. As we give it more structure to assume on `Pickler<'T>`, we can partially evaluate the definitions with that, automatically performing specialization.

2. Semi-automatically unroll the definitions and compute efficient programs for the 2-3-4-5 cases.

3. Figure out how to do rewriting simplifications. 

I can share the Coq code if you are interested. Thanks.