finish writing unzip, learn about let bindings, write theorem about combine_split inverse, prove it, and learn about destructing tuples. pretty cool! (note: split_combine is not inverse because combine cuts off longer lists)