This changes the encoding used for finite lists of values of countable types to be linear instead of exponential. The encoding works by duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then separating each element with 10. The top 1-bits are not kept since we know a 10 is starting a new element which ends with a 1.

Please don't hold back on feedback. I'm sure this could do with some improvements :)